--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/term3.agda.replaced	Tue Nov 02 06:55:58 2021 +0900
@@ -0,0 +1,10 @@
+lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
+10})
+lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning  in
+begin
+(Equal (varn env) c10 ) @$\wedge$@ true
+@$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@
+Equal (varn env) c10
+@$\equiv$@@$\langle$@ cond @$\rangle$@
+true
+@$\blacksquare$@ )