fact: Definition hereditary_type (t : type * term * term) := (term * option { u : type | u = (fst (fst t)) \/ type_subterm u (fst (fst t)) })%type.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat