From dcac7c3f755cb1980e62f517d639d8e12ffd1c76 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Oct 2006 16:47:18 +0000 Subject: [PATCH] till some patches --- .../LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma | 8 ++++++++ .../contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma index 539d32575..15a4e77fd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma @@ -18,6 +18,14 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props". include "iso/fwd.ma". +theorem iso_refl: + \forall (t: T).(iso t t) +\def + \lambda (t: T).(T_ind (\lambda (t0: T).(iso t0 t0)) (\lambda (n: +nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k: +K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_: +(iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t). + theorem iso_trans: \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 t3) \to (iso t1 t3))))) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma index 61c56a0be..83eee6eb2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma @@ -20,7 +20,7 @@ include "nf2/pr3.ma". include "pr3/fwd.ma". -include "iso/fwd.ma". +include "iso/props.ma". theorem nf2_iso_appls_lref: \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs: -- 2.39.2