1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 (* EQUALITY PREDICATE FOR PROOFS IN CONTEXT
20 include "datatypes_defs/Context.ma".
22 inductive PEq (Q1:Context) (p1:Proof) (Q2:Context) (p2:Proof): Prop \def
23 | peq_intro: Q1 = Q2 \land p1 = p2 \to PEq Q1 p1 Q2 p2
26 (*CSC: the URI must disappear: there is a bug now *)
28 "leibniz equality between proofs in context"
30 (cic:/matita/LOGIC/PEq/defs/PEq.ind#xpointer(1/1) x1 y1 x2 y2)
33 notation "hvbox([a1,b1] break = [a2,b2])"
34 non associative with precedence 45
35 for @{ 'eq2 $a1 $b1 $a2 $b2 }.