(**************************************************************************)
include "ground_2/notation/relations/funexteq_2.ma".
-include "ground_2/relocation/nstream_lift.ma".
+include "ground_2/relocation/rtmap.ma".
(* RELOCATION MAP ***********************************************************)
(* Basic properties *********************************************************)
-let corec eq_refl: reflexive … eq ≝ ?.
+corec lemma eq_refl: reflexive … eq.
#f cases (pn_split f) *
#g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
qed.
-let corec eq_sym: symmetric … eq ≝ ?.
+corec lemma eq_sym: symmetric … eq.
#f1 #f2 * -f1 -f2
#f1 #f2 #g1 #g2 #Hf #H1 #H2
[ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
(* Main properties **********************************************************)
-let corec eq_trans: Transitive … eq ≝ ?.
+corec theorem eq_trans: Transitive … eq.
#f1 #f * -f1 -f
#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
/3 width=5 by eq_push, eq_next/
qed-.
-theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2.
+theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≗ f2).
/3 width=3 by eq_trans, eq_sym/ qed-.
-theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2.
+theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≗ f).
/3 width=3 by eq_trans, eq_sym/ qed-.