proposition: Lemma induction_term0 (s:fterm2) a: induction_term s a \0c = a.
proof: Proof. by move: (induction_defined_pr0 s a)=> [sf sjf w0 ws]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)