assumption

assumption solves goals in which there exists an assumption that directly proves the goal (no simplification). This tactic will fail if there does not exist such an assumption.

Syntax

(* Simple usage *)
assumption.

Examples

Before

P: Prop
H: P
-------------------------
1/1
P

assumption

After

Proof finished

Resources

Reference Documentation

---