EC: a = b, fa = fd ⊨ a = c → fb = fc
DC: a = b ∧ ¬ fa = fc ⊨ ¬ b = c
QED=: Ra(fa), a = b ⊨ fb = c → Rbc
QED=: Rab ∧ Rbc, a = b ∨ b = c ⊨ Rbb
Nc=: Fa ∧ ¬ Fb ⊨ ¬ a = b
MPP=: Fb → Ga, Fa ⊨ a = b → Gb