1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Plogic/equality.ma".
17 (* experimental: JMeq support *)
19 ninductive jmeq (A:Type[2]) (a:A) : ∀B:Type[2].B → Prop ≝
20 | refl_jmeq : jmeq A a A a.
22 naxiom jmeq_to_eq : ∀A:Type[2].∀a,b:A.jmeq A a A b → a = b.
24 ncoercion jmeq_to_eq : ∀A:Type[2].∀a,b:A.∀p:jmeq A a A b.a = b ≝
25 jmeq_to_eq on _p: jmeq ???? to eq ???.
27 notation > "hvbox(a break ≃ b)"
28 non associative with precedence 45
29 for @{ 'jmeq ? $a ? $b }.
31 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
32 non associative with precedence 45
33 for @{ 'jmeq $t $a $u $b }.
35 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
37 naxiom streicherKjmeq : ∀T:Type[2].∀t:T.∀P:t ≃ t → Type[2].P (refl_jmeq ? t) → ∀p.P p.