Re: [isabelle] prove set (tl L) ⊆ set L



By calling sledgehammer, which gave me

by (metis (lifting) append_in_lists_conv dual_order.refl lists_eq_set
mem_Collect_eq rotate1_hd_tl set_rotate1 tl.simps(1))

Not a pretty proof, but I got it w/o having to post anything.

Tobias

Am 23/05/2013 18:46, schrieb Roger H.:
> Hello!
> 
> 
> how can i prove this result:
> 
> 
> lemma "set (tl L) ⊆ set L"
> 
> 
> Thank you!
>  		 	   		  
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.