]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/esempio_oliboni.ma
restructuring
[helm.git] / matita / matita / tests / esempio_oliboni.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "logic/equality.ma".
16 include "nat/nat.ma".
17
18 universe constraint Type[0] < Type[1].
19 universe constraint Type[1] < Type[2].
20 universe constraint CProp[0] < CProp[1].
21 universe constraint Type[0] ≤ CProp[0].
22 universe constraint CProp[0] ≤ Type[0].
23 universe constraint Type[1] ≤ CProp[1].
24 universe constraint CProp[1] ≤ Type[1].
25
26 ninductive A : Type[0] ≝ 
27  | K : nat → A
28  | W : nat → A.
29  
30 nlet rec A_rect (Q_:∀x_3:A.Type[0]) H_K H_W x_3 on x_3 :Q_ x_3≝
31 match x_3 with [K x_4⇒H_K x_4|W x_5⇒H_W x_5].
32
33 nlemma yy : ∀x,y. K x = W y → False.
34 #x; #y; #H; 
35 nchange with 
36   (match K x return λ_.Prop with [ K _ ⇒ False | W _ ⇒ True]);
37 nrewrite > H; nwhd; napply I;
38 nqed.  
39   
40 nlemma xx : ∀x,y. K x = K y → x = y.
41 # x; #y; #H;
42 nchange with 
43   (match K x return λ_.Prop with [ K a ⇒ a = y | W b ⇒ b = y]);
44 nrewrite > H; nwhd; napply (refl_eq ??);
45 nqed.
46
47 naxiom P : Prop.
48
49 nlemma ww : ∀a,b:A. a = b → P.
50 #a; #b;
51 ncases a; ncases b;
52 #x; #y; #H;
53 ##[  
54
55 ##| nelim (yy ?? H);
56 ##| nelim (yy ?? H);
57
58 ##]
59
60
61
62