[STATEMENT]
lemma coherent_Lunit'_Ide:
    assumes "Ide a"
    shows "coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]
[PROOF STEP]
using assms Ide_implies_Can coherent_Lunit_Ide
            coherent_iff_coherent_Inv [of "Lunit a"]
[PROOF STATE]
proof (prove)
using this:
Ide a
Ide ?t \<Longrightarrow> Can ?t
Ide ?t \<Longrightarrow> coherent \<^bold>\<l>\<^bold>[?t\<^bold>]
Can \<^bold>\<l>\<^bold>[a\<^bold>] \<Longrightarrow> coherent \<^bold>\<l>\<^bold>[a\<^bold>] = coherent (Inv \<^bold>\<l>\<^bold>[a\<^bold>])

goal (1 subgoal):
 1. coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]
[PROOF STEP]
by simp