Something

  1 proof deMorganNotOr : ~(A | B) => ~A & ~B =  2 begin  3   [~(A | B);  4     [A;  5       A | B;  6       F;  7     ];  8     ~A;  9     [B; 10       A | B; 11       F; 12     ]; 13     ~B; 14     ~A & ~B; 15   ]; 16   ~(A | B) => ~A & ~B; 17 end; 60 proof deMorganAndNot : (~A & ~B) => ~(A | B) = 61 begin 62   [~A & ~B; 63     ~A; 64     ~B; 65     [A | B; 66       [A; 67         F; 68       ]; 69       [B; 70         F; 71       ]; 72       F; 73     ]; 74     ~(A | B); 75   ]; 76   (~A & ~B) => ~(A | B); 77 end;