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

Axiom

logic.eq_ind

Statement

∀ x P, P x ⇒ ∀ y, x = y ⇒ P y

Main Dependencies
constant
Theory
constant

Coq-Jumb
Statement

Axiom eq_ind : forall A, forall (x:A), forall (P:(A -> Prop)), (P x) -> forall (y:A), (eq (A) x y) -> P y



Matita-Jumb
Statement

axiom eq_ind : \forall A. \forall (x:A). \forall (P:A -> Prop). (P x) -> \forall (y:A). ((eq) (A) x y) -> P y



Lean-jumb
Statement

axiom eq_ind : forall (A : Type) , forall (x:A) , forall (P:(A) -> Prop) , ((P) (x)) -> forall (y:A) , ((((logic.eq_) (A)) (x)) (y)) -> (P) (y)



PVS-jumb

Statement

eq_ind [A:TYPE+] : AXIOM (FORALL(x:A):(FORALL(P:[A -> bool]):(P(x) => (FORALL(y:A):(logic_sttfa.eq[A](x)(y) => P(y))))))



OpenTheory

Printing for OpenTheory is not working at the moment.