[STATEMENT]
lemma H_cons: "\<tt>\<tt> p \<le> \<tt>\<tt> p' \<Longrightarrow> \<tt>\<tt> q' \<le> \<tt>\<tt> q \<Longrightarrow> H p' x q' \<Longrightarrow> H p x q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tt>\<tt> p \<le> \<tt>\<tt> p'; \<tt>\<tt> q' \<le> \<tt>\<tt> q; H p' x q'\<rbrakk> \<Longrightarrow> H p x q
[PROOF STEP]
by (simp add: H_consl H_consr)

\<comment> \<open> Skip \<close>