(* *)
(**************************************************************************)
-include "ground_2/xoa/and_4.ma".
-include "ground_2/xoa/ex_4_2.ma".
-include "ground_2/xoa/or_4.ma".
+include "ground/xoa/and_4.ma".
+include "ground/xoa/ex_4_2.ma".
+include "ground/xoa/or_4.ma".
include "static_2/notation/relations/supterm_6.ma".
include "static_2/notation/relations/supterm_7.ma".
include "static_2/syntax/lenv.ma".
(* Basic properties *********************************************************)
-lemma fqu_sort: â\88\80b,I,G,L,s. â\9dªG,L.â\93\98[I],â\8b\86sâ\9d« â¬\82[b] â\9dªG,L,â\8b\86sâ\9d«.
+lemma fqu_sort: â\88\80b,I,G,L,s. â\9d¨G,L.â\93\98[I],â\8b\86sâ\9d© â¬\82[b] â\9d¨G,L,â\8b\86sâ\9d©.
/2 width=1 by fqu_drop/ qed.
-lemma fqu_lref_S: â\88\80b,I,G,L,i. â\9dªG,L.â\93\98[I],#â\86\91iâ\9d« â¬\82[b] â\9dªG,L,#iâ\9d«.
+lemma fqu_lref_S: â\88\80b,I,G,L,i. â\9d¨G,L.â\93\98[I],#â\86\91iâ\9d© â¬\82[b] â\9d¨G,L,#iâ\9d©.
/2 width=1 by fqu_drop/ qed.
-lemma fqu_gref: â\88\80b,I,G,L,l. â\9dªG,L.â\93\98[I],§lâ\9d« â¬\82[b] â\9dªG,L,§lâ\9d«.
+lemma fqu_gref: â\88\80b,I,G,L,l. â\9d¨G,L.â\93\98[I],§lâ\9d© â¬\82[b] â\9d¨G,L,§lâ\9d©.
/2 width=1 by fqu_drop/ qed.
(* Basic inversion lemmas ***************************************************)
-fact fqu_inv_sort1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_sort1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∀s. T1 = ⋆s →
∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
]
qed-.
-lemma fqu_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9dªG1,L1,â\8b\86sâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9d¨G1,L1,â\8b\86sâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
/2 width=4 by fqu_inv_sort1_aux/ qed-.
-fact fqu_inv_lref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_lref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∀i. T1 = #i →
(∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
]
qed-.
-lemma fqu_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9dªG1,L1,#iâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9d¨G1,L1,#iâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
(∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
/2 width=4 by fqu_inv_lref1_aux/ qed-.
-fact fqu_inv_gref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_gref1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∀l. T1 = §l →
∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
]
qed-.
-lemma fqu_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9dªG1,L1,§lâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9d¨G1,L1,§lâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
/2 width=4 by fqu_inv_gref1_aux/ qed-.
-fact fqu_inv_bind1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_bind1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∀p,I,V1,U1. T1 = ⓑ[p,I]V1.U1 →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
]
qed-.
-lemma fqu_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\91[p,I]V1.U1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.U1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
| ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
| ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓑ[p,I]V1.U1.
/2 width=4 by fqu_inv_bind1_aux/ qed-.
-lemma fqu_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\91[p,I]V1.U1â\9d« â¬\82 â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.U1â\9d© â¬\82 â\9d¨G2,L2,T2â\9d© →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2
| ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓑ[p,I]V1.U1.
/3 width=1 by and3_intro, or3_intro1/
qed-.
-fact fqu_inv_flat1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+fact fqu_inv_flat1_aux: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∀I,V1,U1. T1 = ⓕ[I]V1.U1 →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1 = L2 & U1 = T2
]
qed-.
-lemma fqu_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,U1,T2. â\9dªG1,L1,â\93\95[I]V1.U1â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,U1,T2. â\9d¨G1,L1,â\93\95[I]V1.U1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1 = L2 & U1 = T2
| ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓕ[I]V1.U1.
(* Advanced inversion lemmas ************************************************)
-lemma fqu_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9dªG1,â\8b\86,â\93ª[I]â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« → ⊥.
+lemma fqu_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9d¨G1,â\8b\86,â\93ª[I]â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© → ⊥.
#b * #x #G1 #G2 #L2 #T2 #H
[ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
#I [2: #V |3: #i ] #_ #H destruct
qed-.
-lemma fqu_inv_sort1_bind: â\88\80b,I,G1,G2,K,L2,T2,s. â\9dªG1,K.â\93\98[I],â\8b\86sâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_sort1_bind: â\88\80b,I,G1,G2,K,L2,T2,s. â\9d¨G1,K.â\93\98[I],â\8b\86sâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
#b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H
#Z #X #H1 #H2 destruct /2 width=1 by and3_intro/
qed-.
-lemma fqu_inv_zero1_pair: â\88\80b,I,G1,G2,K,L2,V,T2. â\9dªG1,K.â\93\91[I]V,#0â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_zero1_pair: â\88\80b,I,G1,G2,K,L2,V,T2. â\9d¨G1,K.â\93\91[I]V,#0â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∧∧ G1 = G2 & L2 = K & T2 = V.
#b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
#Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
qed-.
-lemma fqu_inv_lref1_bind: â\88\80b,I,G1,G2,K,L2,T2,i. â\9dªG1,K.â\93\98[I],#(â\86\91i)â\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_lref1_bind: â\88\80b,I,G1,G2,K,L2,T2,i. â\9d¨G1,K.â\93\98[I],#(â\86\91i)â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∧∧ G1 = G2 & L2 = K & T2 = #i.
#b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H *
#Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
qed-.
-lemma fqu_inv_gref1_bind: â\88\80b,I,G1,G2,K,L2,T2,l. â\9dªG1,K.â\93\98[I],§lâ\9d« â¬\82[b] â\9dªG2,L2,T2â\9d« →
+lemma fqu_inv_gref1_bind: â\88\80b,I,G1,G2,K,L2,T2,l. â\9d¨G1,K.â\93\98[I],§lâ\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
∧∧ G1 = G2 & L2 = K & T2 = §l.
#b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H
#Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/