| fqu_bind_dx: ∀p,I,G,L,V,T. fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
| fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓧ) T
| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ{I}V.T) G L T
-| fqu_drop : â\88\80I,G,L,T,U. â¬\86*[1] T â\89¡ U → fqu b G (L.ⓘ{I}) U G L T
+| fqu_drop : â\88\80I,G,L,T,U. â¬\86*[1] T â\89\98 U → fqu b G (L.ⓘ{I}) U G L T
.
interpretation
(* Basic properties *********************************************************)
-lemma fqu_lref_S: ∀b,I,G,L,V,i. ⦃G, L.ⓑ{I}V, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄.
+lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #↑i⦄ ⊐[b] ⦃G, L, #i⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄.
/2 width=1 by fqu_drop/ qed.
(* Basic inversion lemmas ***************************************************)
fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀i. T1 = #i →
(∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
- â\88\83â\88\83J,j. G1 = G2 & L1 = L2.â\93\98{J} & T2 = #j & i = ⫯j.
+ â\88\83â\88\83J,j. G1 = G2 & L1 = L2.â\93\98{J} & T2 = #j & i = â\86\91j.
#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/
| #I #G #L #V #T #i #H destruct
lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊐[b] ⦃G2, L2, T2⦄ →
(∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
- â\88\83â\88\83J,j. G1 = G2 & L1 = L2.â\93\98{J} & T2 = #j & i = ⫯j.
+ â\88\83â\88\83J,j. G1 = G2 & L1 = L2.â\93\98{J} & T2 = #j & i = â\86\91j.
/2 width=4 by fqu_inv_lref1_aux/ qed-.
fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
| ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
- | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+ | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{p,I}V1.U1.
#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #T #q #J #V0 #U0 #H destruct
| #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
| ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
- | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+ | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{p,I}V1.U1.
/2 width=4 by fqu_inv_bind1_aux/ qed-.
lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
- | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓑ{p,I}V1.U1.
+ | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓑ{p,I}V1.U1.
#p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H
/3 width=1 by or3_intro0, or3_intro1, or3_intro2/
* #_ #_ #_ #H destruct
∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1 = L2 & U1 = T2
- | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓕ{I}V1.U1.
+ | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓕ{I}V1.U1.
#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #T #J #V0 #U0 #H destruct
| #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/
lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
| ∧∧ G1 = G2 & L1 = L2 & U1 = T2
- | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89¡ ⓕ{I}V1.U1.
+ | â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & â¬\86*[1] T2 â\89\98 ⓕ{I}V1.U1.
/2 width=4 by fqu_inv_flat1_aux/ qed-.
(* Advanced inversion lemmas ************************************************)
#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. â¦\83G1, K.â\93\98{I}, #(⫯i)⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+lemma fqu_inv_lref1_bind: â\88\80b,I,G1,G2,K,L2,T2,i. â¦\83G1, K.â\93\98{I}, #(â\86\91i)⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∧∧ 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/