PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: l disjoint append2
T:Type, a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)
By:
Unfold `l_disjoint` 0
THEN
RWO Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) 0
THEN
Obvious
Generated subgoals:

None

About:
listuniverseandorall

PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc