Library Waterproof.Tactics.Claims

Require Import Ltac2.Ltac2.

Require Import Util.Constr.
Require Import Util.Goals.

Require Import Waterproof.Tactics.Help.

Local Ltac2 my_assert (t:constr) (id:ident option) :=
  
  match id with
    | None =>
      let h := Fresh.in_goal @_H in
      ltac2_assert h t
    | Some id => ltac2_assert id t
  end.

Ltac2 Notation "We" "claim" "that" t(constr) id(opt(seq("(", ident, ")"))) :=
  panic_if_goal_wrapped ();
  
  HelpNewHyp.suggest_how_to_use_after_proof t id;
  my_assert t id.