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 (**************************************************************************)
15 include "ground/relocation/gr_fcla_eq.ma".
16 include "ground/relocation/gr_isf.ma".
18 (* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
20 (* Constructions with gr_eq *************************************************)
22 (*** isfin_eq_repl_back *)
23 lemma gr_isf_eq_repl_back:
24 gr_eq_repl_back … gr_isf.
25 #f1 * /3 width=4 by gr_fcla_eq_repl_back, ex_intro/
28 (*** isfin_eq_repl_fwd *)
29 lemma gr_isf_eq_repl_fwd: gr_eq_repl_fwd … gr_isf.
30 /3 width=3 by gr_isf_eq_repl_back, gr_eq_repl_sym/ qed-.