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