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 (**************************************************************************)
23 notation "#" non associative with precedence 90 for @{ 'sharp }.
24 interpretation "a" 'sharp = a.
25 interpretation "b" 'sharp = b.
27 definition k : A → A ≝ λx.a.
28 definition k1 : A → A ≝ λx.a.
32 include "nat/plus.ma".
34 ntheorem pappo : ∀n:nat.n = S n + n → S n = (S (S n)).
35 #m; #H; napply (let pippo ≝ (S m) in ?);
36 nchange in match (S m) in ⊢ (?) with pippo;
38 nletin pippo ≝ (S m) in H ⊢ (?);
41 nchange in match (S ?) in H:% ⊢ (? → %) with (pred (S ?));
44 ngeneralize in match m in ⊢ %; in ⊢ (???% → ??%?);
46 ncases (O) in m : % (*H : (??%?)*) ⊢ (???%);
47 nelim (S m) in H : (??%?) ⊢ (???%);
50 ntheorem pippo : ∀x:A. P (k x).
51 nchange in match (k x) in ⊢ (∀_.%) with (k1 x); STOP
53 ntheorem prova : (A → A → C) → C.
55 napply (H ? ?); nchange A xxx;