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

Theorem

logic.trans_eq

Statement

∀ x y z, x = y ⇒ y = z ⇒ x = z

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem trans_eq : forall A, forall (x:A), forall (y:A), forall (z:A), (eq (A) x y) -> (eq (A) y z) -> eq (A) x z.



Matita-Jumb
Statement

theorem trans_eq : \forall A. \forall (x:A). \forall (y:A). \forall (z:A). ((eq) (A) x y) -> ((eq) (A) y z) -> (eq) (A) x z.



Lean-jumb
Statement

theorem trans_eq : forall (A : Type) , forall (x:A) , forall (y:A) , forall (z:A) , ((((logic.eq_) (A)) (x)) (y)) -> ((((logic.eq_) (A)) (y)) (z)) -> (((logic.eq_) (A)) (x)) (z).



PVS-jumb

Statement

trans_eq [A:TYPE+] : LEMMA (FORALL(x:A):(FORALL(y:A):(FORALL(z:A):(logic_sttfa.eq[A](x)(y) => (logic_sttfa.eq[A](y)(z) => logic_sttfa.eq[A](x)(z))))))



OpenTheory

Printing for OpenTheory is not working at the moment.