From: Claudio Sacerdoti Coen Date: Thu, 1 Jul 2010 22:01:36 +0000 (+0000) Subject: Proof simplified. X-Git-Tag: make_still_working~2884 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5027bc68bf4f3dc777d35476a2fb8a41b6bc1e29;p=helm.git Proof simplified. --- 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 a1d72698e..44f8e9f21 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -51,17 +51,11 @@ coercion relation_pair_of_relation_pair_setoid. 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; - [ apply (. (commute ?? r')^-1 ??); - apply (. H^-1 ??); - apply (. commute ?? r ??); - assumption; - | apply (. (commute ?? r)^-1 ??); - apply (. H ??); - apply (. commute ?? r' ??); - assumption; - ] + intros 5 (o1 o2 r r' H); + apply (.= (commute ?? r)^-1); + change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); + apply rule (.= H); + apply (commute ?? r'). qed. definition id_relation_pair: ∀o:basic_pair. relation_pair o o.