proposition: Lemma EQ_skel : forall a b : skel, {a = b} + {a <> b}.
proof: Proof. induction a as [| s H s0 H0]; simple destruct b; intros. left; auto with core. right; red in |- *; intros neq; discriminate neq. right; red in |- *; intros neq; discriminate neq. elim H with s1; [ intro Heq1 | intro Hneq1 ]. elim Heq1. elim H0 with s2; [ intro Heq2 | intro Hneq2 ]. elim Heq2. left; auto with core. right; red in |- *; intros; apply Hneq2. injection H1; trivial. right; red in |- *; intros; apply Hneq1. injection H1; trivial. Qed.
imports: Termes Conv Types ListType