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

Theorem

logic.eq_coerc

Statement

∀ A B, A ⇒ A = B ⇒ B

Main Dependencies
Theory
constant

Coq-Jumb
Statement

Theorem eq_coerc : forall (A:Prop), forall (B:Prop), A -> (eq (Prop) A B) -> B.



Matita-Jumb
Statement

theorem eq_coerc : \forall (A:Prop). \forall (B:Prop). (A) -> ((eq) (Prop) A B) -> B.



Lean-jumb
Statement

theorem eq_coerc : forall (A:Prop) , forall (B:Prop) , (A) -> ((((logic.eq_) (Prop)) (A)) (B)) -> B.



PVS-jumb

Statement

eq_coerc : LEMMA (FORALL(A:bool):(FORALL(B:bool):(A => (logic_sttfa.eq[bool](A)(B) => B))))



OpenTheory

Printing for OpenTheory is not working at the moment.