// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

logic.sym_not_eq

Statement

∀ x y, ¬(x = y) ⇒ ¬(y = x)

Main Dependencies
Theory
Coq-Jumb
Statement

Theorem sym_not_eq : forall A, forall (x:A), forall (y:A), (connectives.Not (eq (A) x y)) -> connectives.Not (eq (A) y x).


Matita-Jumb
Statement

theorem sym_not_eq : \forall A. \forall (x:A). \forall (y:A). ((Not) ((eq) (A) x y)) -> (Not) ((eq) (A) y x).


Lean-jumb
Statement

theorem sym_not_eq : forall (A : Type) , forall (x:A) , forall (y:A) , (((connectives.Not) ) ((((logic.eq_) (A)) (x)) (y))) -> ((connectives.Not) ) ((((logic.eq_) (A)) (y)) (x)).


PVS-jumb
Statement

sym_not_eq [A:TYPE+] : LEMMA (FORALL(x:A):(FORALL(y:A):(connectives_sttfa_th.sttfa_Not(logic_sttfa.eq[A](x)(y)) => connectives_sttfa_th.sttfa_Not(logic_sttfa.eq[A](y)(x)))))


OpenTheory

Printing for OpenTheory is not working at the moment.