fact: Record inductive_system: Type := InductiveSystem { isE : Set; isI : Set; isr : Set; isf : Set; is_preorder_r: preorder isr; is_substrate_r: substrate isr = isI; is_directed_r: right_directed_on isr isI; is_fgraph_E: fgraph isE; is_domain_E: domain isE = isI; is_fgraph_f: fgraph isf; is_domain_f: domain isf = isr; is_function_f: forall p, inc p isr -> function_prop (Vg isf p) (Vg isE (P p)) (Vg isE (Q p)); is_compose_f: forall i j k, gle isr i j -> gle isr j k -> Vg isf (J j k) \co Vg isf (J i j) = Vg isf (J i k); is_identity_f: forall i, inc i isI -> Vg isf (J i i) = identity (Vg isE i) }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)