[STATEMENT]
lemma foldli_card: "det_fold_set X (\<lambda>_. True) (\<lambda>_ n. Suc n) 0 card"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_fold_set X (\<lambda>_. True) (\<lambda>_. Suc) 0 card
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>distinct l; sorted_wrt X l\<rbrakk> \<Longrightarrow> foldli l (\<lambda>_. True) (\<lambda>_. Suc) 0 = card (set l)
[PROOF STEP]
using foldli_card_aux[where n=0]
[PROOF STATE]
proof (prove)
using this:
distinct ?l \<Longrightarrow> foldli ?l (\<lambda>_. True) (\<lambda>_. Suc) 0 = 0 + card (set ?l)

goal (1 subgoal):
 1. \<And>l. \<lbrakk>distinct l; sorted_wrt X l\<rbrakk> \<Longrightarrow> foldli l (\<lambda>_. True) (\<lambda>_. Suc) 0 = card (set l)
[PROOF STEP]
by simp