fact: Fixpoint flattenT_R_relation {t : Telescope} : relation (flattenT t X) := match t return relation (flattenT t X) with | bottom => R | tele A B => forall_relation (fun a => flattenT_R_relation) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Relations.Relation_Definitions Coq.Classes.Morphisms