From a773ee47c7539bdbafbfdca306424abaee4a9024 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 20 Oct 2008 14:06:53 +0000 Subject: [PATCH] ... --- .../matita/contribs/didactic/algebra.ma | 28 ++++++------------- 1 file changed, 9 insertions(+), 19 deletions(-) diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma index 3bfa6d7f7..17c30e341 100644 --- a/helm/software/matita/contribs/didactic/algebra.ma +++ b/helm/software/matita/contribs/didactic/algebra.ma @@ -89,23 +89,13 @@ case EPlus. by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11). by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22). the thesis becomes - (∀v. val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v = - val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v). + (∀v. val (subst e1 E1 i) v + val (subst e2 E1 i) v = + val (subst e1 E2 i) v + val (subst e2 E2 i) v). assume v : (ℕ → ℕ). - conclude (val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v) - = (val (EPlus (subst e1 E1 i) (subst e2 E2 i)) v). - = (val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v) by H22. - assume n : ℕ. - the thesis becomes - (equiv - (if (eqb i n) then E1 else (X n)) - (subst (X n) E2 i)). - the thesis becomes - (equiv - (if (eqb i n) then E1 else (X n)) - (if (eqb i n) then E2 else (X n))). - we proceed by cases ... - - - - \ No newline at end of file + conclude + (val (subst e1 E1 i) v + val (subst e2 E1 i) v) = + (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11. + conclude + (val (subst e1 E1 i) v + val (subst e2 E1 i) v) = + (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22. + done. -- 2.39.2