(** * Free-variable lemmas for DOT.
To limit compile times, do not load this file in unary_lr. *)
From D.Dot Require Import syn.
(L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms)
(** Here is a manual proof of [fv_vabs_inv], with explanations, as
documentation for [solve_inv_fv_congruence]. *)
Lemma fv_vabs_inv_manual e n : nclosed_vl (vabs e) n → nclosed e n.+1.
rewrite /nclosed_vl /nclosed => /= Hfv s1 s2 HsEq.
(* From [Hfv], we only learn that [e.|[up s1] = e.|[up s2]], for arbitrary
[s1] and [s2], but substitutions in our thesis [e.|[s1] = e.|[s2]] are not
of form [up ?]. Hence, we rewrite it using [decomp_s] / [decomp_s_vl] to
get a substitution of form [up ?], then rewrite with [e.|[up (stail s1)] =
e.|[up (stail s2)]] (got from [Hfv]), and conclude.
rewrite ?(decomp_s _ s1) ?(decomp_s _ s2) ?(decomp_s_vl _ s1) ?(decomp_s_vl _ s2) (eq_n_s_heads HsEq); last lia.
injection (Hfv _ _ (eq_n_s_tails HsEq)); rewritePremises; reflexivity.
(** The following ones are "direct" lemmas: deduce that an expression is closed
by knowing that its subexpression are closed. *)
Lemma fv_vabs_inv e n : nclosed_vl (vabs e) n → nclosed e n.+1.
Proof. solve_inv_fv_congruence. Qed.