-definition CTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
- λA,B,R,a. TC … (R a).
-
-definition s_r_transitive: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2.
- ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
-
-definition s_rs_transitive: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2.
- ∀L2,T1,T2. CTC … R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
-
-lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
- ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
- ∃∃a. R2 a1 a & TC … R1 a2 a.
+definition CTC (A:Type[0]) (B):
+ (A→relation B) → (A→relation B) ≝
+ λR,a. TC … (R a).
+
+definition s_r_transitive (A) (B):
+ relation2 (A→relation B) (B→relation A) ≝
+ λR1,R2.
+ ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
+
+definition s_rs_transitive (A) (B):
+ relation2 (A→relation B) (B→relation A) ≝
+ λR1,R2.
+ ∀L2,T1,T2. CTC … R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
+
+lemma TC_strip (A) (R1) (R2):
+ confluent2 A R1 R2 →
+ ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & TC … R1 a2 a.