rewrite

rewrite

Coq < Goal forall x, x = 1 -> 2 = 1 + x.
1 subgoal
  
  ============================
   forall x : nat, x = 1 -> 2 = 1 + x

Unnamed_thm3 < intros.
1 subgoal
  
  x : nat
  H : x = 1
  ============================
   2 = 1 + x

Unnamed_thm3 < rewrite H.
1 subgoal
  
  x : nat
  H : x = 1
  ============================
   2 = 1 + 1

Unnamed_thm3 < reflexivity.
Proof completed.

* はてなダイアリーキーワード:rewrite