-
-(* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
-(*
-ninductive peqv (A:Prop) (x:A) : A → Prop ≝
- prefl_eqv : peqv A x x.
-
-interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
-*)
-(* \equiv *)
-(*
-notation > "hvbox(a break ≡ b)"
- non associative with precedence 45
-for @{ 'preqv ? $a $b }.
-
-nlemma symmetric_peqv: ∀A:Prop. symmetric A (peqv A).
- #A;
- nnormalize;
- #x; #y; #H;
- napply (peqv_ind A x (λ_.?) ? y H);
- napply prefl_eqv.
-nqed.
-
-nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P y.
- #A; #x; #P; #H; #y; #H1;
- napply (peqv_ind A x (λ_.?) H y (symmetric_peqv … H1)).
-nqed.
-
-naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
-*)
-(* uso P x → P y, H e' P x
- nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
- nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));
-*)