trivial

trivial is essentially a non-recursive auto. trivial is best utilized when a lemma that exactly matches the goal already exists in the hint database.

Syntax

(* Simple usage *)
trivial.

(* Using a specific database *)
trivial with bool.

Examples

Script

Theorem trivial_example : forall {X : Type} (n : X), 
    n = n.
Proof.
    trivial.
Qed.

Resources

Reference Documentation

---