proposition: Lemma app_eq_nil_inv : forall (A : Set)(ls2 ls1 ls3 : list A), ls1 = ls2 ++ ls3 -> length ls1 = length ls2 -> ls3 = nil.
proof: Proof. induction ls2; intuition; simpl in *; subst. destruct ls3; simpl in *; trivial. lia. simpl in *. eapply IHls2. eauto. lia. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia