From 35a0b2aaeb0413fedbe7de94973167c98222e30e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Feb 2010 07:30:16 +0000 Subject: [PATCH] New proofs. --- helm/software/matita/nlibrary/basics/list.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma index b5664d134..92eddc705 100644 --- a/helm/software/matita/nlibrary/basics/list.ma +++ b/helm/software/matita/nlibrary/basics/list.ma @@ -79,7 +79,9 @@ ntheorem cons_append_commute: //; nqed. ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. -/2/; nqed. +#A; #a; #l; #l1; napply symmetric_eq. +napply associative_append. +(* /2/; *) nqed. ntheorem nil_append_elim: ∀A.∀l1,l2: list A.∀P: list A → list A → Prop. l1@l2 = [] → P (nil A) (nil A) → P l1 l2. -- 2.39.2