From 8423682054bead9ef906bdd8c15d6e0fbd5a2194 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 Jul 2010 21:38:32 +0000 Subject: [PATCH] Proof simplified (??). --- .../formal_topology/overlap/basic_pairs.ma | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma index 0734411f8..a1d72698e 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -53,12 +53,14 @@ lemma eq_to_eq': ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. intros 7 (o1 o2 r r' H c1 f2); split; intro H1; - [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2; - lapply (if ?? (H c1 f2) H2) as H3; - apply (if ?? (commute ?? r' c1 f2) H3); - | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2; - lapply (fi ?? (H c1 f2) H2) as H3; - apply (if ?? (commute ?? r c1 f2) H3); + [ apply (. (commute ?? r')^-1 ??); + apply (. H^-1 ??); + apply (. commute ?? r ??); + assumption; + | apply (. (commute ?? r)^-1 ??); + apply (. H ??); + apply (. commute ?? r' ??); + assumption; ] qed. -- 2.39.2