proposition: Lemma extract_hyps_app : forall l ln1 ln2, extract_hyps l (ln1 ++ ln2) = (extract_hyps l ln1) ++ (extract_hyps l ln2).
proof: Proof. intros l ln1; induction ln1 as [|? ln1 IHln1]. - reflexivity. - simpl. intros. rewrite IHln1. reflexivity. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl