You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I believe one of the concrete suggestions was something like
Require Import StructTact.StructTactics.
Tactic Notation "find_rewrite" "<-" := find_reverse_rewrite.
Goal forall x y z : nat, x = y -> y = z -> x = z.
Proof.
intros.
find_rewrite <-.
assumption.
Qed.
I dont know what this means, but it was suggested and everybody nodded, so I assume its good.
The text was updated successfully, but these errors were encountered: