proposition: Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
proof: Proof. intros gl prf;case_eq (check_proof empty gl prf);intro check_prf. - change (interp_ctx empty F_empty [[gl]]) ; apply interp_proof with prf;assumption. - trivial. Qed.
imports: List Bintree Bool BinPos