stmt2Cond : {c10 :!$\mathbb{N}$!} !$\rightarrow$! Cond
stmt2Cond {c10} env = (Equal (varn env) c10) !$\wedge$! (Equal (vari env) 0)

lemma1 : {c10 :!$\mathbb{N}$!} !$\rightarrow$! Axiom (stmt1Cond {c10})
       (!$\lambda$! env !$\rightarrow$! record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
lemma1 {c10} env = impl!$\Rightarrow$! ( !$\lambda$! cond !$\rightarrow$! let open !$\equiv$!-Reasoning  in
  begin
    ?      -- ?0
  !$\equiv$!!$\langle$! ? !$\rangle$!    -- ?1
    ?      -- ?2
  !$\blacksquare$! )

-- ?0 : Bool
-- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) !$\equiv$! true
-- ?2 : Bool