% prop2.tut
% Idempotency of conjunction
%{
proof idemAnd1 : A & A => A =
begin
[A & A;
A];
A & A => A ;
end;

proof idemAnd2 : A => A & A =
begin
[A;
A & A];
A => A & A ;
end;

proof idemAnd : A & A <=> A =
begin
[A;
A & A];
A => A & A ;
[A & A;
 A];
A & A => A ;
A & A <=> A        % AndI
end;

}%

proof idemAnd : A & A <=> A =
begin
[A;
A & A;
A];
A => A & A ;
A & A => A ;
A & A <=> A        % AndI
end;