1 (* (C) 2014 Luca Bressan *)
5 definition eDe: est → est.
10 | #i * [ 2: #i' @(i ≃ i') | 3,4: #_ #_ ] @falsum
11 | #F1 #F2 #H1 #H2 * [ 3: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 4: #_ #_ ] @falsum
12 | #F1 #F2 #H1 #H2 * [ 4: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 3: #_ #_ ] @falsum
18 | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
19 | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
22 [ * [ #_ % | #i #abs @(De_clash_unit_ev I i abs)
23 | #F1 #F2 #abs @(De_clash_unit_times I F1 F2 abs)
24 | #F1 #F2 #abs @(De_clash_unit_plus I F1 F2 abs) ]
25 | #i * [ @falsum_rect_CProp0 | #i' @sym | 3,4: #F1' #F2' #abs @abs ]
26 | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
27 | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ]
28 | #F1' #F2' #abs @abs ]
29 | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
31 | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ] ]
35 | #i' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_ev I i' abs))
36 | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_times I F1' F2' abs))
37 | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_plus I F1' F2' abs))
39 | #i * [ #F'' @falsum_rect_CProp0
40 | #i' * [ #_ #abs @abs
42 | 3,4: #F1'' #F2'' #_ #abs @abs
44 | 3,4: #F1' #F2' #F'' @falsum_rect_CProp0
46 | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
47 | #i' #F'' @falsum_rect_CProp0
48 | #F1' #F2' * [ #_ #abs @abs
50 | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
51 [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
52 | #F1'' #F2'' #_ #abs @abs
54 | #F1' #F2' #F'' @falsum_rect_CProp0
56 | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
57 | #i' #F'' @falsum_rect_CProp0
58 | #F1' #F2' #F'' @falsum_rect_CProp0
59 | #F1' #F2' * [ #_ #abs @abs
61 | #F1'' #F2'' #_ #abs @abs
62 | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
63 [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]