Exercices 4a

5. Prove the propositions p2 and p3:
   Nb. Adpat the "apply" rule as follow:

let apply (h:string) ((hs,p::ps):Seq):Seq = 
 let v = List.filter (fun (k,r)->k=h) hs
 match v with
 | []               -> (hs,p::ps)
 | (_,Imp (h,q))::_ -> if p=q then (hs,h::ps) else (hs,p::ps)
 | (_,q)::_         -> if p=q then (hs,ps) else (hs,p::ps);;

Answers

([],[p2]) 
  |> intro "h1" 
  |> intro "h2" 
  |> apply "h2" 
  |> apply "h1" 
  |> proven;;

([],[p3]) 
  |> intro "f" 
  |> intro "g" 
  |> intro "x" 
  |> apply "g" 
  |> apply "f" 
  |> apply "x" 
  |> proven;;

6 - 12