Unary Substitution#128

Draft

b4er wants to merge 6 commits intojvanbruegge:masterfrom

b4er:unary-substitution

Commits on Feb 15, 2026

Define unary substitutions and export simp theorems
b4er
committed
Discharge cardinality premises in unary substitution simps
b4er
committed
Get rid of all SSupp, IImssupp, SSupp, and imsupp mentions in unary substitution simps
b4er
committed

Commits on Feb 24, 2026

use nested lthy
dtraytel
committed

Commits on Mar 2, 2026

Simplify subst theorems & fix is_RVr
b4er
committed

Commits on Mar 25, 2026

tidy subst theorems
b4er
committed