val l___example_u946__7_elim__3 : type.
data l_List_18 :=
l_List_18_nil
| l_List_18_cons l___example_u946__7_elim__3 l_List_18.
data l_List_17 :=
l_List_17_nil
| l_List_17_cons l_List_18 l_List_17.
pred l_List_inv__2_spec__39 : ((l___example_u946__7_elim__3 -> prop) -> (l_List_18 -> prop)) :=
(forall (var0 : (l___example_u946__7_elim__3 -> prop)) . ((l_List_inv__2_spec__39 var0) l_List_18_nil));
(forall (var1 : (l___example_u946__7_elim__3 -> prop)) . (forall (var2 : l___example_u946__7_elim__3) . (forall (var3 : l_List_18) . (((var1 var2) && ((l_List_inv__2_spec__39 var1) var3)) => ((l_List_inv__2_spec__39 var1) ((l_List_18_cons var2) var3)))))).
val l___example_u945__6_elim__0 : type.
val l_f : (l___example_u945__6_elim__0 -> l_List_18).
axiom ((fun (var4 : (l___example_u945__6_elim__0 -> l_List_18)) . (forall (var5 : l___example_u945__6_elim__0) . ((l_List_inv__2_spec__39 (fun (var6 : l___example_u946__7_elim__3) . true)) (var4 var5)))) l_f).
data l_Append_22 :=
l_Append_22_mk (l_List_18 -> (l_List_18 -> l_List_18)).
rec l_Append_22_proj__0 : (l_Append_22 -> (l_List_18 -> (l_List_18 -> l_List_18))) :=
(forall (var7 : (l_List_18 -> (l_List_18 -> l_List_18))) . ((l_Append_22_proj__0 (l_Append_22_mk var7)) = var7)).
data l_List_16 :=
l_List_16_nil
| l_List_16_cons l___example_u945__6_elim__0 l_List_16.
pred l_List_inv__2_spec__38 : ((l___example_u945__6_elim__0 -> prop) -> (l_List_16 -> prop)) :=
(forall (var8 : (l___example_u945__6_elim__0 -> prop)) . ((l_List_inv__2_spec__38 var8) l_List_16_nil));
(forall (var9 : (l___example_u945__6_elim__0 -> prop)) . (forall (var10 : l___example_u945__6_elim__0) . (forall (var11 : l_List_16) . (((var9 var10) && ((l_List_inv__2_spec__38 var9) var11)) => ((l_List_inv__2_spec__38 var9) ((l_List_16_cons var10) var11)))))).
val l_xs : l_List_16.
axiom ((l_List_inv__2_spec__38 (fun (var12 : l___example_u945__6_elim__0) . true)) l_xs).
rec l_Append_append_28 : (l_Append_22 -> (l_List_18 -> (l_List_18 -> l_List_18))) :=
(forall (var13 : l_Append_22) . ((l_Append_append_28 var13) = (l_Append_22_proj__0 var13))).
rec l_List_append_33 : (l_List_18 -> (l_List_18 -> l_List_18)) :=
(forall (var14 : l_List_18) . (((l_List_append_33 l_List_18_nil) var14) = var14));
(forall (var15 : l_List_18) . (forall (var16 : l___example_u946__7_elim__3) . (forall (var17 : l_List_18) . (((l_List_append_33 ((l_List_18_cons var16) var17)) var15) = ((l_List_18_cons var16) ((l_List_append_33 var17) var15)))))).
rec l_List_instAppend_32 : l_Append_22 :=
(l_List_instAppend_32 = (l_Append_22_mk l_List_append_33)).
data l_HAppend_27 :=
l_HAppend_27_mk (l_List_18 -> (l_List_18 -> l_List_18)).
rec l_HAppend_27_proj__0 : (l_HAppend_27 -> (l_List_18 -> (l_List_18 -> l_List_18))) :=
(forall (var18 : (l_List_18 -> (l_List_18 -> l_List_18))) . ((l_HAppend_27_proj__0 (l_HAppend_27_mk var18)) = var18)).
rec l_instHAppendOfAppend_26 : (l_Append_22 -> l_HAppend_27) :=
(forall (var19 : l_Append_22) . ((l_instHAppendOfAppend_26 var19) = (l_HAppend_27_mk (fun (var20 : l_List_18) . (fun (var21 : l_List_18) . (((l_Append_append_28 var19) var20) var21)))))).
rec l_HAppend_hAppend_31 : (l_HAppend_27 -> (l_List_18 -> (l_List_18 -> l_List_18))) :=
(forall (var22 : l_HAppend_27) . ((l_HAppend_hAppend_31 var22) = (l_HAppend_27_proj__0 var22))).
rec l_List_flatten_30 : (l_List_17 -> l_List_18) :=
((l_List_flatten_30 l_List_17_nil) = l_List_18_nil);
(forall (var23 : l_List_18) . (forall (var24 : l_List_17) . ((l_List_flatten_30 ((l_List_17_cons var23) var24)) = (((l_HAppend_hAppend_31 (l_instHAppendOfAppend_26 l_List_instAppend_32)) var23) (l_List_flatten_30 var24))))).
rec l_List_map_34 : ((l___example_u945__6_elim__0 -> l_List_18) -> (l_List_16 -> l_List_17)) :=
(forall (var25 : (l___example_u945__6_elim__0 -> l_List_18)) . (((l_List_map_34 var25) l_List_16_nil) = l_List_17_nil));
(forall (var26 : (l___example_u945__6_elim__0 -> l_List_18)) . (forall (var27 : l___example_u945__6_elim__0) . (forall (var28 : l_List_16) . (((l_List_map_34 var26) ((l_List_16_cons var27) var28)) = ((l_List_17_cons (var26 var27)) ((l_List_map_34 var26) var28)))))).
rec l_List_flatMap_29 : ((l___example_u945__6_elim__0 -> l_List_18) -> (l_List_16 -> l_List_18)) :=
(forall (var29 : (l___example_u945__6_elim__0 -> l_List_18)) . (forall (var30 : l_List_16) . (((l_List_flatMap_29 var29) var30) = (l_List_flatten_30 ((l_List_map_34 var29) var30))))).
val l_x : l___example_u945__6_elim__0.
goal (~ (((l_List_flatMap_29 l_f) ((l_List_16_cons l_x) l_xs)) = ((l_List_flatMap_29 l_f) l_xs))).
Error: type error
when applying ((l___example_u945__6_elim__0 -> prop) -> l_List_16 -> prop)
on anon_fun_0, l_xs : (l___example_u946__7_elim__3 -> prop), l_List_16
in subst {}: type mismatch on first argument
causes