sat3: SAT3 mem; (* we add the clusure by rev dapp *)
sat4: SAT4 mem (* we add the clusure by dummies *)
}.
+
(* HIDDEN BUG:
* if SAT0 and SAT1 are expanded,
* the projections sat0 and sat1 are not generated
#C1 #C2 #QC #i (elim i) /3/
qed.
*)
-(* the r.c for a (dependent) product type. ************************************)
+(* the r.c. for a (dependent) product type. ***********************************)
definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
-#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
+#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
qed.
lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
qed.
lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
-#B #C #N #l1 #l2 #HN #M #HM <appl_append >associative_append /3/
+#B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
qed.
lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
#B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
[ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
qed.
+
+(* the union of two r.c.'s. ***************************************************)
+
+definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
+
+lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
+#B #C #M #Hlor elim Hlor -Hlor #HM /2/
+qed.
+
+lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
+#B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
+qed.
+
+lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
+#B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
+qed.
+
+lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
+#B #C #N #HN elim HN -HN #HN /3/
+qed.
+
+definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
+/2/ qed.