set -> type

[helm.git] / helm / software / matita / library / Fsub / part1a.ma

diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index e12a64be4809093d647ba9f04a8906d42d2a9f83..795546299e842f8c2f2824a7c102db04e548d5d1 100644 (file)
--- a/helm/software/matita/library/Fsub/part1a.ma
+++ b/helm/software/matita/library/Fsub/part1a.ma
@@ -176,7 +176,7 @@ cut (\forall G,T,Q.(JSubtype G T Q) \to
                  |simplify;apply incl_nat_cons;assumption]]]
         |elim G2 0
            [simplify;unfold;intros;assumption
-           |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]]
+           |intro;elim t 0;simplify;intros;apply incl_nat_cons;assumption]]]
   |intros 4;(*generalize in match H1;*)elim H1
      [inversion H5
         [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)