ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
+
+(* 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)));
+*)