Functional Programming & Proofs

Exercices 4a

Prove the following expressions

A &&& B ==> B &&& A
(A &&& B ==> C)  <=> (A ===> (B ===>C))
((A===>B) &&& (C ===> D)) <=> ((A&&&C)==>(B&&&D))

Answers

([],[p]) 
  |> intro "h" 
  |> destruct "h" "h1" "h2" 
  |> split
  |> apply "h2" 
  |> apply "h1";;

([],[((A &&& B) ==> C)  ==> (A ===> (B ===>C))])
  |> intro "h" |> intro "a" |> intro "b" |> apply "h" 
  |> split |> apply "a" |> apply "b";;

8 - 12