Metamath Proof Explorer
Table of Contents - 5.7.5. Concatenations with singleton words
- ccatws1cl
- ccatws1clv
- ccat2s1cl
- ccats1alpha
- ccatws1len
- ccatws1lenp1b
- wrdlenccats1lenm1
- ccat2s1len
- ccat2s1lenOLD
- ccatw2s1cl
- ccatw2s1len
- ccats1val1
- ccats1val1OLD
- ccats1val2
- ccat1st1st
- ccat2s1p1
- ccat2s1p2
- ccat2s1p1OLD
- ccat2s1p2OLD
- ccatw2s1ass
- ccatw2s1assOLD
- ccatws1n0
- ccatws1ls
- lswccats1
- lswccats1fst
- ccatw2s1p1
- ccatw2s1p1OLD
- ccatw2s1p2
- ccat2s1fvw
- ccat2s1fvwOLD
- ccat2s1fst
- ccat2s1fstOLD