(* Basic properties ***********************************************************)
lemma frees_teqg_conf_seqg (S):
- â\88\80f,L1,T1. L1 â\8a¢ ð\9d\90\85+â\9dªT1â\9d« ≘ f → ∀T2. T1 ≛[S] T2 →
- â\88\80L2. L1 â\89\9b[S,f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9dªT2â\9d« ≘ f.
+ â\88\80f,L1,T1. L1 â\8a¢ ð\9d\90\85+â\9d¨T1â\9d© ≘ f → ∀T2. T1 ≛[S] T2 →
+ â\88\80L2. L1 â\89\9b[S,f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9d¨T2â\9d© ≘ f.
#S #f #L1 #T1 #H elim H -f -L1 -T1
[ #f #L1 #s1 #Hf #X #H1 #L2 #_
elim (teqg_inv_sort1 … H1) -H1 #s2 #_ #H destruct
lemma frees_teqg_conf (S):
reflexive … S →
- â\88\80f,L,T1. L â\8a¢ ð\9d\90\85+â\9dªT1â\9d« ≘ f →
- â\88\80T2. T1 â\89\9b[S] T2 â\86\92 L â\8a¢ ð\9d\90\85+â\9dªT2â\9d« ≘ f.
+ â\88\80f,L,T1. L â\8a¢ ð\9d\90\85+â\9d¨T1â\9d© ≘ f →
+ â\88\80T2. T1 â\89\9b[S] T2 â\86\92 L â\8a¢ ð\9d\90\85+â\9d¨T2â\9d© ≘ f.
/5 width=6 by frees_teqg_conf_seqg, sex_refl, teqg_refl, ext2_refl/ qed-.
lemma frees_seqg_conf (S):
reflexive … S →
- â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f →
- â\88\80L2. L1 â\89\9b[S,f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f.
+ â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f →
+ â\88\80L2. L1 â\89\9b[S,f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f.
/3 width=6 by frees_teqg_conf_seqg, teqg_refl/ qed-.
lemma teqg_rex_conf_sn (S) (R):
/2 width=1 by rex_pair/ qed.
lemma reqg_unit (S):
- â\88\80f,I,L1,L2. ð\9d\90\88â\9dªfâ\9d« → L1 ≛[S,f] L2 →
+ â\88\80f,I,L1,L2. ð\9d\90\88â\9d¨fâ\9d© → L1 ≛[S,f] L2 →
L1.ⓤ[I] ≛[S,#0] L2.ⓤ[I].
/2 width=3 by rex_unit/ qed.
∀Y1,Y2. Y1 ≛[S,#0] Y2 →
∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
| ∃∃I,L1,L2,V1,V2. L1 ≛[S,V1] L2 & V1 ≛[S] V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
- | â\88\83â\88\83f,I,L1,L2. ð\9d\90\88â\9dªfâ\9d« & L1 ≛[S,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
+ | â\88\83â\88\83f,I,L1,L2. ð\9d\90\88â\9d¨fâ\9d© & L1 ≛[S,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
#S #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.