-lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
-/2/ qed.
-
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
- P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
- ∀a2. TC … R a1 a2 → P a2.
-#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
-qed.
-
-definition NF: ∀A. relation A → relation A → A → Prop ≝