- @(subset_eq_trans ā¦ (unwind2_term_fsubst ā¦))
- [ @fsubst_eq_repl [ // | // ]
- @(subset_eq_trans ā¦ (unwind2_term_iref ā¦))
- @(subset_eq_canc_sn ā¦ (lift_term_eq_repl_dx ā¦))
- [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
- @(subset_eq_trans ā¦ (unwind2_lift_term_after ā¦))
- @unwind2_term_eq_repl_sn
+ @(subset_eq_trans ā¦ (lift_term_fsubst ā¦))
+ @fsubst_eq_repl [ // | // ]
+ @(subset_eq_trans ā¦ (lift_term_iref ā¦))
+ @iref_eq_repl
+ @(subset_eq_canc_sn ā¦ (lift_term_grafted_S ā¦))
+ @lift_term_eq_repl_sn