[STATEMENT]
lemma lemma_3_5_ii_1 [simp]: "d1 a a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d1 a a = (1::'a)
[PROOF STEP]
apply (subst lemma_3_5_i_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a
[PROOF STEP]
by simp