IV. Logic and proofs

3. We define two transformations rules to:

a. introduce an hypothesis

let intro (h:string):Seq->Seq = function
 | (hs,(Imp(p,q))::ps) -> ((h,p)::hs,q::ps)
 | s                   -> s;;

let s2 = intro "h1" s1;; // = ???

"Introduction" can only be applied to "Implication A=>B" and says "admit A and proove B".

3 - 12