@@ -67,11+67,11 @@ fact frees_inv_atom_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀i. L = ⋆
]
qed-.
]
qed-.
-lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i]⫯g.
+lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i]â\86\91g.
/2 width=5 by frees_inv_atom_aux/ qed-.
/2 width=5 by frees_inv_atom_aux/ qed-.
-fact frees_inv_pair_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & f = ⫯g.
+fact frees_inv_pair_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & f = â\86\91g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #X #_ #H destruct
| #f #i #_ #Z #Y #X #H destruct
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #X #_ #H destruct
| #f #i #_ #Z #Y #X #H destruct
@@ -84,11+84,11 @@ fact frees_inv_pair_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,V. L = K.
]
qed-.
]
qed-.
-lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & f = ⫯g.
+lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & f = â\86\91g.
/2 width=6 by frees_inv_pair_aux/ qed-.
/2 width=6 by frees_inv_pair_aux/ qed-.
-fact frees_inv_unit_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,K. L = K.ⓤ{I} → X = #0 →
- â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯g.
+fact frees_inv_unit_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,K. L = K.ⓤ{I} → X = #0 →
+ â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #_ #H destruct
| #f #i #_ #Z #Y #H destruct
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #_ #H destruct
| #f #i #_ #Z #Y #H destruct
@@ -101,11+101,11 @@ fact frees_inv_unit_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K. L = K.
]
qed-.
]
qed-.
-lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤{I} â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯g.
+lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤{I} â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91g.
/2 width=7 by frees_inv_unit_aux/ qed-.
/2 width=7 by frees_inv_unit_aux/ qed-.
-fact frees_inv_lref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f â\86\92 â\88\80I,K,j. L = K.â\93\98{I} â\86\92 X = #(⫯j) →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#jâ¦\84 â\89¡ g & f = â\86\91g.
+fact frees_inv_lref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,K,j. L = K.â\93\98{I} â\86\92 X = #(â\86\91j) →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#jâ¦\84 â\89\98 g & f = ⫯g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #j #_ #H destruct
| #f #i #_ #Z #Y #j #H destruct
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #j #_ #H destruct
| #f #i #_ #Z #Y #j #H destruct
@@ -118,11+118,11 @@ fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,j. L = K.
]
qed-.
]
qed-.
-lemma frees_inv_lref: â\88\80f,I,K,i. K.â\93\98{I} â\8a¢ ð\9d\90\85*â¦\83#(⫯i)â¦\84 â\89¡ f →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ g & f = â\86\91g.
+lemma frees_inv_lref: â\88\80f,I,K,i. K.â\93\98{I} â\8a¢ ð\9d\90\85*â¦\83#(â\86\91i)â¦\84 â\89\98 f →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 g & f = ⫯g.
/2 width=6 by frees_inv_lref_aux/ qed-.
/2 width=6 by frees_inv_lref_aux/ qed-.
-fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀x. X = §x → 𝐈⦃f⦄.
+fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀x. X = §x → 𝐈⦃f⦄.
#f #L #X #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
#f #L #X #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
@@ -133,11+133,11 @@ fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x
]
qed-.
]
qed-.
-lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89¡ f → 𝐈⦃f⦄.
+lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89\98 f → 𝐈⦃f⦄.
/2 width=5 by frees_inv_gref_aux/ qed-.
/2 width=5 by frees_inv_gref_aux/ qed-.
-fact frees_inv_bind_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+fact frees_inv_bind_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.
#f #L #X * -f -L -X
[ #f #L #s #_ #q #J #W #U #H destruct
| #f #i #_ #q #J #W #U #H destruct
#f #L #X * -f -L -X
[ #f #L #s #_ #q #J #W #U #H destruct
| #f #i #_ #q #J #W #U #H destruct
@@ -150,12+150,12 @@ fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀p,I,V,T. X =
]
qed-.
]
qed-.
-lemma frees_inv_bind: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+lemma frees_inv_bind: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.
/2 width=4 by frees_inv_bind_aux/ qed-.
/2 width=4 by frees_inv_bind_aux/ qed-.
-fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,V,T. X = ⓕ{I}V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 f2 â\89¡ f.
+fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,V,T. X = ⓕ{I}V.T →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 f2 â\89\98 f.
#f #L #X * -f -L -X
[ #f #L #s #_ #J #W #U #H destruct
| #f #i #_ #J #W #U #H destruct
#f #L #X * -f -L -X
[ #f #L #s #_ #J #W #U #H destruct
| #f #i #_ #J #W #U #H destruct
@@ -168,13+168,13 @@ fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X =
]
qed-.
]
qed-.
-lemma frees_inv_flat: â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\95{I}V.Tâ¦\84 â\89¡ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 f2 â\89¡ f.
+lemma frees_inv_flat: â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\95{I}V.Tâ¦\84 â\89\98 f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 f2 â\89\98 f.