[STATEMENT]
lemma struct_specI:
  assumes "sel_spec sel" and "ap_spec ap" and "ab_spec ab" and "compl_struct compl"
  shows "struct_spec sel ap ab compl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. struct_spec sel ap ab compl
[PROOF STEP]
unfolding struct_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sel_spec sel \<and> ap_spec ap \<and> ab_spec ab \<and> compl_struct compl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sel_spec sel
ap_spec ap
ab_spec ab
compl_struct compl

goal (1 subgoal):
 1. sel_spec sel \<and> ap_spec ap \<and> ab_spec ab \<and> compl_struct compl
[PROOF STEP]
by (intro conjI)