+inductive jmeq (A:Type[1]) (x:A) : ∀B:Type[1]. B →Prop ≝
+refl_jmeq : jmeq A x A x.
+
+notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
+ non associative with precedence 45
+for @{ 'jmsimeq $t $a $u $b }.
+
+notation > "hvbox(n break ≃ m)"
+ non associative with precedence 45
+for @{ 'jmsimeq ? $n ? $m }.
+
+interpretation "john major's equality" 'jmsimeq t x u y = (jmeq t x u y).
+interpretation "john major's reflexivity" 'refl = refl_jmeq.