proposition: Lemma eq_can_trans : forall (s : skel) (a b c : Can s), eq_can s a b -> eq_can s b b -> eq_can s b c -> eq_can s a c.
proof: Proof. simple induction s; simpl in |- *; intros. unfold eq_cand in |- *; intros. elim H with t; elim H1 with t; auto with coc core arith datatypes. apply H0 with (b X1); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class