% prop3.tut
% Classical implication definition  ~A|B => A=>B

proof ImpDef : ~A|B => A=>B =
begin
[~A|B;
  [A;
    [~A;
      F;	
      B];
    [B;	
     B];
   B;
  ];
  A => B];
~A|B => A=>B	
end;



%{
[ ~A|B;
  [ A;
    [ ~A;
      F;	
      B	];	
    [ B;
      B	];	
    B ];		
  A=>B ];	
}%