From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 20:06:29 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5154
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11852aa9c64848457d84af63186d2317772e74bf;p=helm.git

Dummy dependent types are no longer cleaned in inductive type arities.
---

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
index 95c832efd..184166ed9 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/defn".
 include "Fsub/util.ma".
 
 (*** representation of Fsub types ***)  
@@ -153,18 +152,19 @@ intros 2;elim G
   [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin
   |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3)
      [rewrite < H4;simplify;apply in_list_head
-     |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a);
-      apply (ex_intro ? ? a1);assumption]]
+     |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a1);
+      apply (ex_intro ? ? a2);assumption]]
 qed.
 
 lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
                               \exists B,T.(in_list ? (mk_bound B x T) G).
 intros 2;elim G 0
   [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
-  |intros 3;elim t;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
-     [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_list_head
-     |elim (H H2);elim H3;apply (ex_intro ? ? a);
-      apply (ex_intro ? ? a1);apply in_list_cons;assumption]]
+  |intros 3;
+   elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+     [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t);apply in_list_head
+     |elim (H H2);elim H3;apply (ex_intro ? ? a1);
+      apply (ex_intro ? ? a2);apply in_list_cons;assumption]]
 qed.
 
 lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to 
@@ -200,7 +200,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G.
                           (fv_env (H @ ((mk_bound B x T) :: G))) = 
                           (fv_env (H @ ((mk_bound C x U) :: G))).
 intros;elim H
-  [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity]
+  [simplify;reflexivity|elim a;simplify;rewrite > H1;reflexivity]
 qed.
 
 lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
@@ -237,12 +237,12 @@ cut (\forall l:(list nat).\exists n.\forall m.
   |intros;elim l
     [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1)
     |elim H;
-     apply (ex_intro ? ? (S (max a t))).
+     apply (ex_intro ? ? (S (max a1 a))).
      intros.unfold. intro.
      elim (in_list_cons_case ? ? ? ? H3)
       [rewrite > H4 in H2.autobatch
       |elim H4
-         [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch
+         [apply (H1 m ? H4).apply (trans_le ? (max a1 a));autobatch
          |assumption]]]]
 qed.
 
@@ -309,7 +309,7 @@ intros 7;elim H 0
   [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros
      [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4)
      |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)]
-  |intros;simplify;generalize in match H2;elim t;simplify in H4;
+  |intros;simplify;generalize in match H2;elim a;simplify in H4;
    inversion H4;intros
      [destruct H5
      |destruct H9;apply WFE_cons
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
index fc3621618..7ae8763cf 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/part1a/".
 include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
index b538f4d3a..5a472e640 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/part1a_inversion/".
 include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
index bd7018d3c..3521e87dd 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/util".
 include "logic/equality.ma".
 include "nat/compare.ma".
 include "list/list.ma".
@@ -55,4 +54,4 @@ lemma max_case : \forall m,n.(max m n) = match (leb m n) with
       [ true \Rightarrow n
       | false \Rightarrow m ].
 intros;elim m;simplify;reflexivity;
-qed.
\ No newline at end of file
+qed.