proposition: Lemma cons_eq : forall x x' : A, forall l l', x = x' -> l = l' -> x :: l = x' :: l'.
proof: Proof. intros. rewrite H, H0. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)