proposition: Lemma eq_can_sym : forall (s : skel) (X Y : Can s), eq_can s X Y -> eq_can s Y X.
proof: Proof. simple induction s; simpl in |- *; intros; auto with coc core arith datatypes. unfold eq_cand in |- *; intros. elim H with t; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class