lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
(∀a,b1. R a b1 b2 → Q a b1) →
(∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
∀a,b1. ltc … f … R a b1 b2 → Q a b1.
lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
(∀a,b1. R a b1 b2 → Q a b1) →
(∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
∀a,b1. ltc … f … R a b1 b2 → Q a b1.