proposition: Lemma F'_ext : forall x (f g : forall y, R y x -> flatten_forall (P' y)), (forall y (p : R y x), flatten_forall_eq (f y p) (g y p)) -> flatten_forall_eq (@F' x f) (@F' x g).
proof: Proof. intros x f' g' IH. subst F' transfer transfer'; cbv beta. apply (_ : Proper (forall_relation _ ==> _) flatten_forall_unapply); intro. apply flatten_forall_apply_Proper. apply F_ext; intros. refine ((_ : Proper (flatten_forall_eq ==> _) (@flatten_forall_eq_rect _ _ _ _)) _ _ _). apply (_ : Proper (forall_relation _ ==> _) flatten_forall_unapply); intro. apply flatten_forall_apply_Proper. apply IH. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Fiat.Common.Telescope.Core Fiat.Common.Telescope.Instances Fiat.Common.Telescope.Equality Fiat.Common Fiat.Common.Equality