- |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
- [ napply f_closed; nassumption ##| napply (. ?‡#) [##2: nassumption | ##3: ##skip]
- nwhd; napply f_closed; nassumption]##]
- #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
- [##2: napply (f_inj … E'); nassumption
- | #E''; nrewrite < E''; napply conj
- [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''')
+ |##1: @ (fi i1 i2); @;
+ ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1".
+napply (. E‡#);
+ nwhd; napply f_closed; nassumption]##]
+ #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
+ #E''; nrewrite < E''; @;
+ ##[ @;
+ ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''')