[STATEMENT]
lemma from_sparse_inj: "inj from_sparse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>(n, v). (n, v, n, PhiDef))
[PROOF STEP]
by (rule injI, auto)


[STATEMENT]
lemma foldr_prod: "foldr (\<lambda>x y. (f1 x (fst y), f2 x (snd y))) xs y = (foldr f1 xs (fst y), foldr f2 xs (snd y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. (f1 x (fst y), f2 x (snd y))) xs y = (foldr f1 xs (fst y), foldr f2 xs (snd y))
[PROOF STEP]
by (induction xs, auto)