Verwenden von eq_refl, um eine "x = x" Hypothese zu erhalten

Question

Kurz gesagt, ist das möglich?

Ich versuche zu beweisen, dass die Stornierung in einer Gruppe funktioniert.

Ich habe

a, b, x : G 
H: a <+> x = b <+> x 

und ich möchte

a = b 

Meine Idee beweisen, wurde die Hypothese

H2: a <+> x <+> i x = a <+> x <+> i x 

(i ist die Umkehrfunktion) zu erhalten.

---

Ich habe

versucht

pose proof eq_refl (a <+> x <+> i x) as H. 

aber das scheint nicht zu funktionieren.

Answer 1

Wenn Ihr Ziel wirklich aussieht wie das, was Sie gepostet haben, dann sollte Ihre Taktik fehlschlagen, weil sie den Namen H wieder verwendet. Wenn dies nicht das Problem ist, dann hilft es zu wissen, welche Fehlermeldung Coq anzeigt.