proposition: Lemma cand_sn : is_cand sn.
proof: Proof. apply Build_is_cand; intros; auto with coc core arith datatypes. apply sn_red_sn with t; auto with coc core arith datatypes. red in |- *; apply Acc_intro; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class