fact: Fixpoint flatten_forall_eq_rect_trans {t : Telescope} : forall {P Q R : flattenT t Type} (p : flattenT_eq P Q) (q : flattenT_eq Q R) (f : flatten_forall P), flatten_forall_eq (flatten_forall_eq_rect (transitivity p q) f) (flatten_forall_eq_rect q (flatten_forall_eq_rect p f)).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Fiat.Common.Equality Fiat.Common.Telescope.Core Fiat.Common.Telescope.Instances