notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
-lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed.
+lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
(* Esercizio 3
===========