proposition: Lemma valid_check_forall_inst (lemma : Prop) : lemma -> forall concl, (lemma -> interp_uf rho concl) -> C.valid rho concl.
proof: Proof. intros pl concl applemma. unfold C.valid. rewrite interp_equiv. now apply applemma. Qed.
imports: State SMT_terms List Bool PArray Int63