proposition: Lemma simple_combine_app_app : forall T (l1 l2 l3 l4 : list T), length l1 = length l3 -> combine (l1 ++ l2) (l3 ++ l4) = combine l1 l3 ++ combine l2 l4.
proof: Proof. induction l1; simpl; introv len; destruct l3; allsimpl; cpx. rw IHl1; sp. Qed.
imports: AlphaEquality SwapProps Eqdep_dec