[STATEMENT]
lemma adjoint_funcs_skip: "SFuncs \<sigma> f=None \<Longrightarrow> Funcs (adjoint \<sigma> I \<omega>) f = Funcs I f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFuncs \<sigma> f = undeft \<Longrightarrow> Funcs (USubst.adjoint \<sigma> I \<omega>) f = Funcs I f
[PROOF STEP]
using adjoint_funcs
[PROOF STATE]
proof (prove)
using this:
Funcs (USubst.adjoint ?\<sigma> ?I ?\<omega>) ?f = (case SFuncs ?\<sigma> ?f of None \<Rightarrow> Funcs ?I ?f | Some r \<Rightarrow> \<lambda>d. term_sem (repc ?I dotid d) r ?\<omega>)

goal (1 subgoal):
 1. SFuncs \<sigma> f = undeft \<Longrightarrow> Funcs (USubst.adjoint \<sigma> I \<omega>) f = Funcs I f
[PROOF STEP]
by auto