(* Basic properties ***********************************************************)
-lemma frees_tdeq_conf_rdeq: โf,L1,T1. L1 โข ๐
*โฆT1โฆ โ f โ โT2. T1 โ T2 โ
- โL2. L1 โ[f] L2 โ L2 โข ๐
*โฆT2โฆ โ f.
+lemma frees_tdeq_conf_rdeq: โf,L1,T1. L1 โข ๐
+โฆT1โฆ โ f โ โT2. T1 โ T2 โ
+ โL2. L1 โ[f] L2 โ L2 โข ๐
+โฆT2โฆ โ f.
#f #L1 #T1 #H elim H -f -L1 -T1
[ #f #L1 #s1 #Hf #X #H1 #L2 #_
elim (tdeq_inv_sort1 โฆ H1) -H1 #s2 #H destruct
]
qed-.
-lemma frees_tdeq_conf: โf,L,T1. L โข ๐
*โฆT1โฆ โ f โ
- โT2. T1 โ T2 โ L โข ๐
*โฆT2โฆ โ f.
+lemma frees_tdeq_conf: โf,L,T1. L โข ๐
+โฆT1โฆ โ f โ
+ โT2. T1 โ T2 โ L โข ๐
+โฆT2โฆ โ f.
/4 width=7 by frees_tdeq_conf_rdeq, sex_refl, ext2_refl/ qed-.
-lemma frees_rdeq_conf: โf,L1,T. L1 โข ๐
*โฆTโฆ โ f โ
- โL2. L1 โ[f] L2 โ L2 โข ๐
*โฆTโฆ โ f.
+lemma frees_rdeq_conf: โf,L1,T. L1 โข ๐
+โฆTโฆ โ f โ
+ โL2. L1 โ[f] L2 โ L2 โข ๐
+โฆTโฆ โ f.
/2 width=7 by frees_tdeq_conf_rdeq, tdeq_refl/ qed-.
lemma tdeq_rex_conf (R): s_r_confluent1 โฆ cdeq (rex R).
qed-.
lemma tdeq_rex_div (R): โT1,T2. T1 โ T2 โ
- โL1,L2. L1 โชค[R, T2] L2 โ L1 โชค[R, T1] L2.
+ โL1,L2. L1 โชค[R,T2] L2 โ L1 โชค[R,T1] L2.
/3 width=5 by tdeq_rex_conf, tdeq_sym/ qed-.
lemma tdeq_rdeq_conf: s_r_confluent1 โฆ cdeq rdeq.
L1 โ[V1] L2 โ V1 โ V2 โ L1.โ{I}V1 โ[#0] L2.โ{I}V2.
/2 width=1 by rex_pair/ qed.
(*
-lemma rdeq_unit: โf,I,L1,L2. ๐โฆfโฆ โ L1 โชค[cdeq_ext, cfull, f] L2 โ
+lemma rdeq_unit: โf,I,L1,L2. ๐โฆfโฆ โ L1 โชค[cdeq_ext,cfull,f] L2 โ
L1.โค{I} โ[#0] L2.โค{I}.
/2 width=3 by rex_unit/ qed.
*)
โจโจ โงโง Y1 = โ & Y2 = โ
| โโI,L1,L2,V1,V2. L1 โ[V1] L2 & V1 โ V2 &
Y1 = L1.โ{I}V1 & Y2 = L2.โ{I}V2
- | โโf,I,L1,L2. ๐โฆfโฆ & L1 โชค[cdeq_ext h o, cfull, f] L2 &
+ | โโf,I,L1,L2. ๐โฆfโฆ & L1 โชค[cdeq_ext h o,cfull,f] L2 &
Y1 = L1.โค{I} & Y2 = L2.โค{I}.
#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/