- ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc;
- ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
- ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
- ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
- [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
+ nlapply (covers ? P); *; #_; #Hc;
+ nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
+ nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
+ nlapply (f_sur ???? (fi nindex) y ?)
+ [ alias symbol "refl" = "refl".
+alias symbol "prop1" = "prop11".
+alias symbol "prop2" = "prop21 mem".
+napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]