(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: l disjoint cons
T:Type, a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b)
By:
Unfold `l_disjoint` 0
THEN
RWO Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0
Generated subgoals:

11. T: Type
2. a: T List
3. b: T List
4. t: T
5. x:T. (x = t (x a) & (x b))
(t b)		1 step
 
21. T: Type
2. a: T List
3. b: T List
4. t: T
5. x:T. (x = t (x a) & (x b))
6. x: T
((x a) & (x b))		1 step
 
31. T: Type
2. a: T List
3. b: T List
4. t: T
5. (t b)
6. x:T. ((x a) & (x b))
7. x: T
(x = t (x a) & (x b))		1 step

About:
listconsuniverseequalandorall

(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc