lego/example.l


1
2
3
4
5
6
7

Module Walkthrough Import lib_logic;
Goal and_commutes: {A,B:Prop}(and A B) -> (and B A);
intros;andI;
Refine H;intros;Immed;Refine H;intros; Immed;
Save and_commutes;