Theory "utils"

Parents     indexedLists   patternMatches

Theorems

child_parent_lemma_2_1_2_3
|- ∀P1 P2 a. (λa. P1 a) a ∧ (λa. P2 a) a ⇔ (λa. P1 a ∧ P2 a) a
LCOMM_THM_gen
|- ∀f P.
     (∀x y z. P x y ∧ P x z ⇒ P x (f y z)) ∧
     (∀x y z. f x (f y z) = f (f x y) z) ∧ (∀x y. P x y ⇒ (f x y = f y x)) ⇒
     ∀x y z. P x y ∧ P x z ⇒ (f x (f y z) = f y (f x z))