From f261b8315d0b14781ae78740feb476327083d664 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 11 May 2009 16:20:24 +0000 Subject: [PATCH] A few lemmas about inclusion. --- helm/software/matita/library/list/in.ma | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma index d6c165022..310c3f369 100644 --- a/helm/software/matita/library/list/in.ma +++ b/helm/software/matita/library/list/in.ma @@ -152,4 +152,16 @@ qed. lemma incl_A_A: ∀T,A.incl T A A. intros.unfold incl.intros.assumption. +qed. + +lemma incl_append_l : ∀T,A,B.incl T A (A @ B). +unfold incl; intros;autobatch. +qed. + +lemma incl_append_r : ∀T,A,B.incl T B (A @ B). +unfold incl; intros;autobatch. +qed. + +lemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. qed. \ No newline at end of file -- 2.39.2