(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/realisability/".
-
include "logic/connectives.ma".
include "datatypes/constructors.ma".
match s return λs.P (pi1 ? ? s) with
[ sigma_intro _ p ⇒ p].
-notation "hvbox(Σ ident i opt (: ty) break . p)"
+notation "hvbox(\Sigma ident i opt (: ty) break . p)"
right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p}
intro;
elim F; simplify;
[1,2: apply H
- | split;
+ | split; simplify in r H2;
[apply H;
[ apply (\fst r)
| apply (proj1 ? ? H2)
]
- | apply H1;
+ | apply H1;simplify in r H2;
[ apply (\snd r)
| apply (proj2 ? ? H2)
]
]
- | generalize in match H2; clear H2;
- change in r with (type_OF_SP s + type_OF_SP s1);
- elim r; simplify in H2;
+ | change in r with (type_OF_SP s + type_OF_SP s1);
+ elim r in H2 ⊢ %; simplify in H2;
[ left; apply H; assumption
| right; apply H1; assumption
]
| skip
]
| simplify in r;
- generalize in match H1; clear H1;
- elim r;
+ elim r in H1 ⊢ %;
apply (ex_intro ? ? a);
apply H;
assumption