fact: Fixpoint extract_hyps (l: list NFormula) (ln : list nat) : list NFormula := match ln with | nil => nil | n::ln => nth n l (Pc cO, Equal) :: extract_hyps l ln end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl