∧true : { x : Bool } → x ∧ true ≡ x ∧true {x} with x ∧true {x} | false = refl ∧true {x} | true = refl stmt1Cond : {c10 :ℕ} → Cond stmt1Cond {c10} env = Equal (varn env) c10