fact: Definition FixV_rect (Q : forall a, flattenT (Telescope_append (B a) (P a)) Type) (H0 : forall x, (forall y, R y x -> flatten_append_forall (@Q y) (@FixV F y)) -> flatten_append_forall (@Q x) (@F x (fun (y : A) (_ : R y x) => @FixV F y))) (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)) a : flatten_append_forall (@Q a) (@FixV F a).
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