From aff6791b3666237a8f95f2eb9d877c1b89b03161 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:30:44 +0000 Subject: [PATCH] ... --- matita/tests/applys.ma | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/matita/tests/applys.ma b/matita/tests/applys.ma index d9cbc9098..c929e5be5 100644 --- a/matita/tests/applys.ma +++ b/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.2