helm/software/matita/nlibrary/Plogic/jmeq.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Plogic/equality.ma".
  16
  17 (* experimental: JMeq support *)
  18
  19 ninductive jmeq (A:Type[2]) (a:A) : ∀B:Type[2].B → Prop ≝
  20 | refl_jmeq : jmeq A a A a.
  21
  22 naxiom jmeq_to_eq : ∀A:Type[2].∀a,b:A.jmeq A a A b → a = b.
  23
  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 ???.
  26
  27 notation > "hvbox(a break ≃ b)"
  28   non associative with precedence 45
  29 for @{ 'jmeq ? $a ? $b }.
  30
  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 }.
  34
  35 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
  36
  37 naxiom streicherKjmeq : ∀T:Type[2].∀t:T.∀P:t ≃ t → Type[2].P (refl_jmeq ? t) → ∀p.P p.