From f48faa46342b557486e06c17fd574d1eeb386239 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 18:22:24 +0000 Subject: [PATCH] Dummy dependent types are no longer cleaned in inductive type arities. --- helm/software/matita/library/list/in.ma | 10 +++++----- helm/software/matita/library/list/list.ma | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma index 0e3be3a8f..d6c165022 100644 --- a/helm/software/matita/library/list/in.ma +++ b/helm/software/matita/library/list/in.ma @@ -99,7 +99,7 @@ lemma mem_true_to_in_list : \forall x,l.mem A equ x l = true \to in_list A x l. intros 5.elim l [simplify in H1;destruct H1 - |simplify in H2;apply (bool_elim ? (equ x t)) + |simplify in H2;apply (bool_elim ? (equ x a)) [intro;rewrite > (H ? ? H3);apply in_list_head |intro;rewrite > H3 in H2;simplify in H2; apply in_list_cons;apply H1;assumption]] @@ -113,14 +113,14 @@ intros 5.elim l [elim (not_in_list_nil ? ? H1) |elim H2 [simplify;rewrite > H;reflexivity - |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]]. + |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. qed. lemma in_list_filter_to_p_true : \forall l,x,p. in_list nat x (filter nat l p) \to p x = true. intros 3;elim l [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1; + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; simplify in H1 [elim (in_list_cons_case ? ? ? ? H1) [rewrite > H3;assumption @@ -131,7 +131,7 @@ qed. lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l. intros 3;elim l [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1; + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; simplify in H1 [elim (in_list_cons_case ? ? ? ? H1) [rewrite > H3;apply in_list_head @@ -145,7 +145,7 @@ intros 3;elim l [elim (not_in_list_nil ? ? H) |elim (in_list_cons_case ? ? ? ? H1) [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head - |simplify;apply (bool_elim ? (p t));intro;simplify; + |simplify;apply (bool_elim ? (p a));intro;simplify; [apply in_list_cons;apply H;assumption |apply H;assumption]]] qed. diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index a180cbabc..ad44bd63a 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -186,13 +186,13 @@ qed. lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. intros (A B f g l Efg); elim l; simplify; [1: reflexivity ]; -rewrite > (Efg t); rewrite > H; reflexivity; +rewrite > (Efg a); rewrite > H; reflexivity; qed. lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l. intros;elim l [simplify;apply le_n - |simplify;apply (bool_elim ? (p t));intro + |simplify;apply (bool_elim ? (p a));intro [simplify;apply le_S_S;assumption |simplify;apply le_S;assumption]] qed. \ No newline at end of file -- 2.39.2