proposition: Lemma app_second_eq : forall (A : Type) (ls2 ls1 ls3 : list A), ls1 = ls2 ++ ls3 -> length ls1 = length ls3 -> ls1 = ls3 /\ ls2 = nil.
proof: Proof. induction ls2; simpl in *; intuition; subst; simpl in *; rewrite app_length in H0; lia. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia