proposition: Lemma flatten_append_forall_Proper {B P Q} : forall f g, @flatten_forall_eq B P f g -> @flatten_append_forall B P Q f -> @flatten_append_forall B P Q g.
proof: Proof. induction B; simpl in *; eauto with nocore. intros; subst; assumption. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Fiat.Common.Telescope.Core