proposition: Lemma clos_red_star : forall R : term -> Prop, is_cand R -> forall a b : term, R a -> red a b -> R b.
proof: Proof. simple induction 3; intros; auto with coc core arith datatypes. apply (clos_red R) with P; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class