fact: Definition proper_statement (s: signature) : chain_type s -> Prop := match s with | gen_F _ => fun ch => Fchain_proper ch | gen_K _ _ => fun ch => Kchain_proper ch end.
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)