From 0663e736012a6bf2af56758181252289e79352d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:30:44 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/applys.ma | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/software/matita/tests/applys.ma b/helm/software/matita/tests/applys.ma index d9cbc9098..c929e5be5 100644 --- a/helm/software/matita/tests/applys.ma +++ b/helm/software/matita/tests/applys.ma @@ -30,5 +30,10 @@ qed. theorem prova2 : \forall n. S n \divides (S n)!. intros. +(* o fare una List.rev quando si fa la make_passives... la tira su, + ma tardi.... +letin www \def sym_times. +clearbody www. +*) applyS (witness ? ? ? (refl_eq ? ?)). qed. -- 2.39.5