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".
+ [ alias symbol "refl" (instance 3) = "refl".
+alias symbol "prop2" (instance 2) = "prop21".
+alias symbol "prop1" (instance 4) = "prop11".
napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);