From 552bdad5b59b096af0e0bbefc660e5f8b0d6c2ec Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Jan 2006 11:26:28 +0000 Subject: [PATCH] Hand-made generated inversion lemma. It heavily uses the new tinycal features. --- helm/matita/tests/inversion2.ma | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/helm/matita/tests/inversion2.ma b/helm/matita/tests/inversion2.ma index 1125212dc..65dc75d40 100644 --- a/helm/matita/tests/inversion2.ma +++ b/helm/matita/tests/inversion2.ma @@ -24,6 +24,25 @@ inductive le (n:nat) : nat \to Prop \def leO : le n n | leS : \forall m. le n m \to le n (S m). +theorem le_inv: + \forall n,m. + \forall P: nat -> nat -> Prop. + ? -> ? -> le n m -> P n m. +[7: + intros; + inversion H; + [ apply x + | simplify; + apply x1 + ] +| skip +| skip +| skip +| skip +| skip +| skip +] +qed. inductive ledx : nat \to nat \to Prop \def ledxO : \forall n. ledx n n -- 2.39.2