renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lsubf.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma

index 62b114915f9097c3447d12bae64ec9c7179bfef4..6eec912778c74fa1b267e8265f17433f6145c643 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -19,15 +19,15 @@ include "basic_2/static/frees.ma".
  (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
  
  inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
-| lsubf_atom: â\88\80f1,f2. f1 â\89\97 f2 → lsubf (⋆) f1 (⋆) f2
+| lsubf_atom: â\88\80f1,f2. f1 â\89¡ f2 → lsubf (⋆) f1 (⋆) f2
  | lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) →
-              lsubf (L1.â\93\98{I1}) (â\86\91f1) (L2.â\93\98{I2}) (â\86\91f2)
+              lsubf (L1.â\93\98{I1}) (â«¯f1) (L2.â\93\98{I2}) (â«¯f2)
  | lsubf_bind: ∀f1,f2,I,L1,L2. lsubf L1 f1 L2 f2 →
-              lsubf (L1.â\93\98{I}) (â«¯f1) (L2.â\93\98{I}) (â«¯f2)
-| lsubf_beta: â\88\80f,f0,f1,f2,L1,L2,W,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f â\86\92 f0 â\8b\93 f â\89¡ f1 →
-              lsubf L1 f0 L2 f2 â\86\92 lsubf (L1.â\93\93â\93\9dW.V) (â«¯f1) (L2.â\93\9bW) (â«¯f2)
-| lsubf_unit: â\88\80f,f0,f1,f2,I1,I2,L1,L2,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f â\86\92 f0 â\8b\93 f â\89¡ f1 →
-              lsubf L1 f0 L2 f2 â\86\92 lsubf (L1.â\93\91{I1}V) (â«¯f1) (L2.â\93¤{I2}) (â«¯f2)
+              lsubf (L1.â\93\98{I}) (â\86\91f1) (L2.â\93\98{I}) (â\86\91f2)
+| lsubf_beta: â\88\80f,f0,f1,f2,L1,L2,W,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f â\86\92 f0 â\8b\93 f â\89\98 f1 →
+              lsubf L1 f0 L2 f2 â\86\92 lsubf (L1.â\93\93â\93\9dW.V) (â\86\91f1) (L2.â\93\9bW) (â\86\91f2)
+| lsubf_unit: â\88\80f,f0,f1,f2,I1,I2,L1,L2,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f â\86\92 f0 â\8b\93 f â\89\98 f1 →
+              lsubf L1 f0 L2 f2 â\86\92 lsubf (L1.â\93\91{I1}V) (â\86\91f1) (L2.â\93¤{I2}) (â\86\91f2)
  .
  
  interpretation
@@ -37,7 +37,7 @@ interpretation
  (* Basic inversion lemmas ***************************************************)
  
  fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
-                          f1 â\89\97 f2 ∧ L2 = ⋆.
+                          f1 â\89¡ f2 ∧ L2 = ⋆.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ /2 width=1 by conj/
  | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
@@ -47,12 +47,12 @@ fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_atom1: â\88\80f1,f2,L2. â¦\83â\8b\86, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 f1 â\89\97 f2 ∧ L2 = ⋆.
+lemma lsubf_inv_atom1: â\88\80f1,f2,L2. â¦\83â\8b\86, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 f1 â\89¡ f2 ∧ L2 = ⋆.
  /2 width=3 by lsubf_inv_atom1_aux/ qed-.
  
  fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g1,I1,K1. f1 = â\86\91g1 → L1 = K1.ⓘ{I1} →
-                          â\88\83â\88\83g2,I2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓘ{I2}.
+                          â\88\80g1,I1,K1. f1 = â«¯g1 → L1 = K1.ⓘ{I1} →
+                          â\88\83â\88\83g2,I2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓘ{I2}.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct
  | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct
@@ -63,18 +63,18 @@ fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_push1: â\88\80g1,f2,I1,K1,L2. â¦\83K1.â\93\98{I1}, â\86\91g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       â\88\83â\88\83g2,I2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓘ{I2}.
+lemma lsubf_inv_push1: â\88\80g1,f2,I1,K1,L2. â¦\83K1.â\93\98{I1}, â«¯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       â\88\83â\88\83g2,I2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓘ{I2}.
  /2 width=6 by lsubf_inv_push1_aux/ qed-.
  
  fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g1,I,K1,X. f1 = â«¯g1 → L1 = K1.ⓑ{I}X →
-                          â\88¨â\88¨ â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓑ{I}X
+                          â\88\80g1,I,K1,X. f1 = â\86\91g1 → L1 = K1.ⓑ{I}X →
+                          â\88¨â\88¨ â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓑ{I}X
                             | ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                               K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2 &
+                                               K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2 &
                                                 I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
                             | ∃∃g,g0,g2,J,K2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                             K1 â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2 &
+                                             K1 â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2 &
                                               L2 = K2.ⓤ{J}.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
@@ -88,19 +88,19 @@ fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_pair1: â\88\80g1,f2,I,K1,L2,X. â¦\83K1.â\93\91{I}X, â«¯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       â\88¨â\88¨ â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓑ{I}X
+lemma lsubf_inv_pair1: â\88\80g1,f2,I,K1,L2,X. â¦\83K1.â\93\91{I}X, â\86\91g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       â\88¨â\88¨ â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓑ{I}X
                          | ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                            K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2 &
+                                            K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2 &
                                              I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
                          | ∃∃g,g0,g2,J,K2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                          K1 â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2 &
+                                          K1 â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2 &
                                            L2 = K2.ⓤ{J}.
  /2 width=5 by lsubf_inv_pair1_aux/ qed-.
  
  fact lsubf_inv_unit1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g1,I,K1. f1 = â«¯g1 → L1 = K1.ⓤ{I} →
-                          â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓤ{I}.
+                          â\88\80g1,I,K1. f1 = â\86\91g1 → L1 = K1.ⓤ{I} →
+                          â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓤ{I}.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct
  | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (discr_push_next … H)
@@ -111,12 +111,12 @@ fact lsubf_inv_unit1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_unit1: â\88\80g1,f2,I,K1,L2. â¦\83K1.â\93¤{I}, â«¯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2 & L2 = K2.ⓤ{I}.
+lemma lsubf_inv_unit1: â\88\80g1,f2,I,K1,L2. â¦\83K1.â\93¤{I}, â\86\91g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       â\88\83â\88\83g2,K2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2 & L2 = K2.ⓤ{I}.
  /2 width=5 by lsubf_inv_unit1_aux/ qed-.
  
  fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
-                          f1 â\89\97 f2 ∧ L1 = ⋆.
+                          f1 â\89¡ f2 ∧ L1 = ⋆.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ /2 width=1 by conj/
  | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
@@ -126,12 +126,12 @@ fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_atom2: â\88\80f1,f2,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83â\8b\86, f2â¦\84 â\86\92 f1 â\89\97 f2 ∧ L1 = ⋆.
+lemma lsubf_inv_atom2: â\88\80f1,f2,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83â\8b\86, f2â¦\84 â\86\92 f1 â\89¡ f2 ∧ L1 = ⋆.
  /2 width=3 by lsubf_inv_atom2_aux/ qed-.
  
  fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g2,I2,K2. f2 = â\86\91g2 → L2 = K2.ⓘ{I2} →
-                          â\88\83â\88\83g1,I1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓘ{I1}.
+                          â\88\80g2,I2,K2. f2 = â«¯g2 → L2 = K2.ⓘ{I2} →
+                          â\88\83â\88\83g1,I1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓘ{I1}.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct
  | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct
@@ -142,15 +142,15 @@ fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_push2: â\88\80f1,g2,I2,L1,K2. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93\98{I2}, â\86\91g2⦄ →
-                       â\88\83â\88\83g1,I1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓘ{I1}.
+lemma lsubf_inv_push2: â\88\80f1,g2,I2,L1,K2. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93\98{I2}, â«¯g2⦄ →
+                       â\88\83â\88\83g1,I1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓘ{I1}.
  /2 width=6 by lsubf_inv_push2_aux/ qed-.
  
  fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g2,I,K2,W. f2 = â«¯g2 → L2 = K2.ⓑ{I}W →
-                          â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓑ{I}W
+                          â\88\80g2,I,K2,W. f2 = â\86\91g2 → L2 = K2.ⓑ{I}W →
+                          â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓑ{I}W
                             | ∃∃g,g0,g1,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
-                                             K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f1 = â«¯g1 &
+                                             K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f1 = â\86\91g1 &
                                               I = Abst & L1 = K1.ⓓⓝW.V.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct
@@ -163,18 +163,18 @@ fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_pair2: â\88\80f1,g2,I,L1,K2,W. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93\91{I}W, â«¯g2⦄ →
-                       â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓑ{I}W
+lemma lsubf_inv_pair2: â\88\80f1,g2,I,L1,K2,W. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93\91{I}W, â\86\91g2⦄ →
+                       â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓑ{I}W
                          | ∃∃g,g0,g1,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
-                                          K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f1 = â«¯g1 &
+                                          K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f1 = â\86\91g1 &
                                            I = Abst & L1 = K1.ⓓⓝW.V.
  /2 width=5 by lsubf_inv_pair2_aux/ qed-.
  
  fact lsubf_inv_unit2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          â\88\80g2,I,K2. f2 = â«¯g2 → L2 = K2.ⓤ{I} →
-                          â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓤ{I}
+                          â\88\80g2,I,K2. f2 = â\86\91g2 → L2 = K2.ⓤ{I} →
+                          â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓤ{I}
                             | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                               K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f1 = â«¯g1 &
+                                               K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f1 = â\86\91g1 &
                                                 L1 = K1.ⓑ{J}V.
  #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
@@ -187,27 +187,27 @@ fact lsubf_inv_unit2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  ]
  qed-.
  
-lemma lsubf_inv_unit2: â\88\80f1,g2,I,L1,K2. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93¤{I}, â«¯g2⦄ →
-                       â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â«¯g1 & L1 = K1.ⓤ{I}
+lemma lsubf_inv_unit2: â\88\80f1,g2,I,L1,K2. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83K2.â\93¤{I}, â\86\91g2⦄ →
+                       â\88¨â\88¨ â\88\83â\88\83g1,K1. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f1 = â\86\91g1 & L1 = K1.ⓤ{I}
                          | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & 
-                                            K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f1 = â«¯g1 &
+                                            K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f1 = â\86\91g1 &
                                              L1 = K1.ⓑ{J}V.
  /2 width=5 by lsubf_inv_unit2_aux/ qed-.
  
  (* Advanced inversion lemmas ************************************************)
  
-lemma lsubf_inv_atom: â\88\80f1,f2. â¦\83â\8b\86, f1â¦\84 â«\83ð\9d\90\85* â¦\83â\8b\86, f2â¦\84 â\86\92 f1 â\89\97 f2.
+lemma lsubf_inv_atom: â\88\80f1,f2. â¦\83â\8b\86, f1â¦\84 â«\83ð\9d\90\85* â¦\83â\8b\86, f2â¦\84 â\86\92 f1 â\89¡ f2.
  #f1 #f2 #H elim (lsubf_inv_atom1 … H) -H //
  qed-.
  
-lemma lsubf_inv_push_sn: â\88\80g1,f2,I1,I2,K1,K2. â¦\83K1.â\93\98{I1}, â\86\91g1⦄ ⫃𝐅* ⦃K2.ⓘ{I2}, f2⦄ →
-                         â\88\83â\88\83g2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2.
+lemma lsubf_inv_push_sn: â\88\80g1,f2,I1,I2,K1,K2. â¦\83K1.â\93\98{I1}, â«¯g1⦄ ⫃𝐅* ⦃K2.ⓘ{I2}, f2⦄ →
+                         â\88\83â\88\83g2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2.
  #g1 #f2 #I #K1 #K2 #X #H elim (lsubf_inv_push1 … H) -H
  #g2 #I #Y #H0 #H2 #H destruct /2 width=3 by ex2_intro/
  qed-.
  
-lemma lsubf_inv_bind_sn: â\88\80g1,f2,I,K1,K2. â¦\83K1.â\93\98{I}, â«¯g1⦄ ⫃𝐅* ⦃K2.ⓘ{I}, f2⦄ →
-                         â\88\83â\88\83g2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â«¯g2.
+lemma lsubf_inv_bind_sn: â\88\80g1,f2,I,K1,K2. â¦\83K1.â\93\98{I}, â\86\91g1⦄ ⫃𝐅* ⦃K2.ⓘ{I}, f2⦄ →
+                         â\88\83â\88\83g2. â¦\83K1, g1â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & f2 = â\86\91g2.
  #g1 #f2 * #I [2: #X ] #K1 #K2 #H
  [ elim (lsubf_inv_pair1 … H) -H *
    [ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
@@ -219,8 +219,8 @@ lemma lsubf_inv_bind_sn: ∀g1,f2,I,K1,K2. ⦃K1.ⓘ{I}, ⫯g1⦄ ⫃𝐅* ⦃K2
  ]
  qed-.
  
-lemma lsubf_inv_beta_sn: â\88\80g1,f2,K1,K2,V,W. â¦\83K1.â\93\93â\93\9dW.V, â«¯g1⦄ ⫃𝐅* ⦃K2.ⓛW, f2⦄ →
-                         â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2.
+lemma lsubf_inv_beta_sn: â\88\80g1,f2,K1,K2,V,W. â¦\83K1.â\93\93â\93\9dW.V, â\86\91g1⦄ ⫃𝐅* ⦃K2.ⓛW, f2⦄ →
+                         â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2.
  #g1 #f2 #K1 #K2 #V #W #H elim (lsubf_inv_pair1 … H) -H *
  [ #z2 #Y2 #_ #_ #H destruct
  | #z #z0 #z2 #Y2 #X0 #X #H02 #Hz #Hg1 #H #_ #H0 #H1 destruct
@@ -229,8 +229,8 @@ lemma lsubf_inv_beta_sn: ∀g1,f2,K1,K2,V,W. ⦃K1.ⓓⓝW.V, ⫯g1⦄ ⫃𝐅*
  ]
  qed-.
  
-lemma lsubf_inv_unit_sn: â\88\80g1,f2,I,J,K1,K2,V. â¦\83K1.â\93\91{I}V, â«¯g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
-                         â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & g0 â\8b\93 g â\89¡ g1 & f2 = â«¯g2.
+lemma lsubf_inv_unit_sn: â\88\80g1,f2,I,J,K1,K2,V. â¦\83K1.â\93\91{I}V, â\86\91g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
+                         â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2.
  #g1 #f2 #I #J #K1 #K2 #V #H elim (lsubf_inv_pair1 … H) -H *
  [ #z2 #Y2 #_ #_ #H destruct
  | #z #z0 #z2 #Y2 #X0 #X #_ #_ #_ #_ #_ #_ #H destruct
@@ -239,7 +239,7 @@ lemma lsubf_inv_unit_sn: ∀g1,f2,I,J,K1,K2,V. ⦃K1.ⓑ{I}V, ⫯g1⦄ ⫃𝐅*
  ]
  qed-.
  
-lemma lsubf_inv_refl: â\88\80L,f1,f2. â¦\83L,f1â¦\84 â«\83ð\9d\90\85* â¦\83L,f2â¦\84 â\86\92 f1 â\89\97 f2.
+lemma lsubf_inv_refl: â\88\80L,f1,f2. â¦\83L,f1â¦\84 â«\83ð\9d\90\85* â¦\83L,f2â¦\84 â\86\92 f1 â\89¡ f2.
  #L elim L -L /2 width=1 by lsubf_inv_atom/
  #L #I #IH #f1 #f2 #H12
  elim (pn_split f1) * #g1 #H destruct
@@ -302,7 +302,7 @@ lemma lsubf_refl: bi_reflexive … lsubf.
  /2 width=1 by lsubf_push, lsubf_bind/
  qed.
  
-lemma lsubf_refl_eq: â\88\80f1,f2,L. f1 â\89\97 f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
+lemma lsubf_refl_eq: â\88\80f1,f2,L. f1 â\89¡ f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
  /2 width=3 by lsubf_eq_repl_back2/ qed.
  
  lemma lsubf_bind_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
@@ -312,20 +312,20 @@ elim (pn_split f2) * #g2 #H2 destruct
  @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
  qed-.
  
-lemma lsubf_beta_tl_dx: â\88\80f,f0,g1,L1,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f â\86\92 f0 â\8b\93 f â\89¡ g1 →
+lemma lsubf_beta_tl_dx: â\88\80f,f0,g1,L1,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f â\86\92 f0 â\8b\93 f â\89\98 g1 →
                          ∀f2,L2,W. ⦃L1, f0⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
                          ∃∃f1. ⦃L1.ⓓⓝW.V, f1⦄ ⫃𝐅* ⦃L2.ⓛW, f2⦄ & ⫱f1 ⊆ g1.
  #f #f0 #g1 #L1 #V #Hf #Hg1 #f2
  elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
  [ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
-| @(ex2_intro â\80¦ (â«¯g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) 
+| @(ex2_intro â\80¦ (â\86\91g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) 
  ]
  qed-.
  
  (* Note: this might be moved *)
  lemma lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                        â\88\80f2l,f2r. f2lâ\8b\93f2r â\89¡ f2 →
-                        â\88\83â\88\83f1l,f1r. â¦\83L1, f1lâ¦\84 â«\83ð\9d\90\85* â¦\83L2, f2lâ¦\84 & â¦\83L1, f1râ¦\84 â«\83ð\9d\90\85* â¦\83L2, f2râ¦\84 & f1lâ\8b\93f1r â\89¡ f1.
+                        â\88\80f2l,f2r. f2lâ\8b\93f2r â\89\98 f2 →
+                        â\88\83â\88\83f1l,f1r. â¦\83L1, f1lâ¦\84 â«\83ð\9d\90\85* â¦\83L2, f2lâ¦\84 & â¦\83L1, f1râ¦\84 â«\83ð\9d\90\85* â¦\83L2, f2râ¦\84 & f1lâ\8b\93f1r â\89\98 f1.
  #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
  [ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/
  | #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H