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