proposition: Lemma length_app_3 {A} : forall n1 n2 n3 (l1 l2 l3 : list A), length l1 = n1 -> length l2 = n2 -> length l3 = n3 -> length (l1 ++ l2 ++ l3) = n1 + n2 + n3.
proof: Proof. intros; rewrite !app_length; subst; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts