Intuitively, Adjoin a k l holds if it is possible to insert the element a in the list k and obtain the list l. This relation can be used to define permutations, as seen below.
** Module lib_list_Adjoin Imports lib_list_length $Adjoin : {s|Type}s->(list s)->(list s)->Prop $ad1 : {s|Type}{a:s}{xs:list s}Adjoin a xs (cons a xs) $ad2 : {s|Type}{xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s} Adjoin a (cons b xs) (cons b axs) $Adjoin_elim : {s|Type}{C_Adjoin:s->(list s)->(list s)->Prop} ({a:s}{xs:list s}C_Adjoin a xs (cons a xs))-> ({xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s} (C_Adjoin a xs axs)->C_Adjoin a (cons b xs) (cons b axs))->{x1|s} {x2,x3|list s}(Adjoin x1 x2 x3)->C_Adjoin x1 x2 x3 [[s|Type][C_Adjoin:s->(list s)->(list s)->Prop] [f_ad1:{a1:s}{xs1:list s}C_Adjoin a1 xs1 (cons a1 xs1)] [f_ad2:{xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s} (C_Adjoin a xs axs)->C_Adjoin a (cons b xs) (cons b axs)][a1:s] [xs1:list s][xs|list s][a|s][axs|list s][x1:Adjoin a xs axs][b:s] Adjoin_elim C_Adjoin f_ad1 f_ad2 (ad1 a1 xs1) ==> f_ad1 a1 xs1 || Adjoin_elim C_Adjoin f_ad1 f_ad2 (ad2 x1 b) ==> f_ad2 x1 b (Adjoin_elim C_Adjoin f_ad1 f_ad2 x1)] Adjoin_inv = ... : {s|Type}{a|s}{xs,ys|list s}(Adjoin a xs ys)-> (Eq ys (cons a xs) \/ Ex ([xs':list s] Ex ([ys':list s] Ex ([c:s] (Eq xs (cons c xs') /\ Eq ys (cons c ys') /\ Adjoin a xs' ys'))))) Adjoin_inv_corr1 = ... : {s|Type}{a,b|s}{xs,ys|list s}(Adjoin a (cons b xs) ys)-> (Eq ys (cons a (cons b xs)) \/ Ex ([ys':list s](Eq ys (cons b ys') /\ Adjoin a xs ys'))) Adjoin_inv_corr2 = ... : {s|Type}{a,b|s}{xs,ys|list s}(Adjoin a xs (cons b ys))-> ((Eq a b /\ Eq xs ys) \/ Ex ([xs':list s](Eq xs (cons b xs') /\ Adjoin a xs' ys))) Adjoin_inv_corr3 = ... : {s|Type}{a|s}{xs|list s}(Adjoin a (nil s) xs)-> Eq xs (cons a (nil s)) Adjoin_inv_corr4 = ... : {s|Type}{a|s}{xs|list s}not (Adjoin a xs (nil s)) Adjoin_inv_corr5 = ... : {s|Type}{a|s}{xs|list s}(Adjoin a xs (cons a (nil s)))-> Eq xs (nil s) Adjoin_com1 = ... : {s|Type}{a,b|s}{xs,us,ys|list s}(Adjoin a xs ys)->(Adjoin b ys us)-> Ex ([zs:list s](Adjoin b xs zs /\ Adjoin a zs us)) Adjoin_com2 = ... : {s|Type}{a,b|s}{xs,us,zs|list s}(Adjoin b zs xs)->(Adjoin a zs us)-> Ex ([ys:list s](Adjoin a xs ys /\ Adjoin b us ys)) Adjoin_com3 = ... : {s|Type}{a,b|s}{xs,us,ys|list s}(Adjoin a xs ys)->(Adjoin b us ys)-> ((Eq us xs /\ Eq b a) \/ Ex ([zs:list s](Adjoin b zs xs /\ Adjoin a zs us))) Adjoin_length_suc = ... : {s|Type}{a|s}{l,al|list s}(Adjoin a l al)-> Eq (length al) (suc (length l))