1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/paramodulation/".
19 definition make_eqs_smart \def
23 let rec aux (p:Univ) (n:nat) on n : Prop \def
25 [ O \Rightarrow \forall a:Univ. p = a \to initial = a
26 | (S n) \Rightarrow \forall a:Univ. p = a \to aux a n
31 theorem transl_smart :
32 \forall Univ:Type.\forall n:nat.\forall initial:Univ.
33 make_eqs_smart Univ n initial.
35 unfold make_eqs_smart.
37 [ simplify.intros.assumption
38 | simplify.intros.rewrite < H1.assumption
45 \forall plus: Univ \to Univ \to Univ.
46 \forall H:\forall x,y:Univ.plus x y = plus y x.
47 \forall H1:plus b a = plus b b.
50 apply (transl_smart ? (S O) ? ? (H a b) ? H1).