proposition: Lemma valid_check_hole: C.valid rho (check_hole s prem_id prem concl).
proof: Proof. unfold check_hole. revert prem p. induction prem_id as [ |pid pids IHpids]; simpl; intros [ |p ps]; simpl; intro H. - unfold C.valid. now rewrite interp_equiv. - now apply C.interp_true. - now apply C.interp_true. - case_eq (forallb2 (fun i j => i =? j) (S.get s pid) (S.sort_uniq p)); simpl; intro Heq; [ |now apply C.interp_true]. apply IHpids. apply H. apply (valid_check_clause _ _ Heq). Qed.
imports: State SMT_terms List Bool PArray Int63