proposition: Lemma alien_sub_cap : forall t, sub (alien_sub t) (cap t) = t.
proof: Proof. intro. pattern t. apply term_ind_forall; intros. simpl. apply alien_sub_var. unfold alien_sub, cap, fresh_for. set (m := maxvar (Fun f v)). simpl. case (defined f R). change (fsub m (Vcons (Fun f v) Vnil) (S m) = Fun f v). apply fsub_cons. lia. set (cs := Vmap capa v). change (let (n,p) := mkCap (fun ts => Fun f (Vmap_sum cs ts), conc cs) in let (f0,v0) := p in sub (fsub m v0) (f0 (fresh (S m) n)) = Fun f v). set (s := mkCap (fun ts => Fun f (Vmap_sum cs ts), conc cs)). assert (s = mkCap (fun ts => Fun f (Vmap_sum cs ts), conc cs)). refl. destruct s. destruct p as [f0 v0]. injection H0. intros. subst x. assert (v0 = conc cs). apply (@inj_existT _ eq_nat_dec (fun x => terms x)). hyp. assert (f0 = fun ts => Fun f (Vmap_sum cs ts)). apply (@inj_existT _ eq_nat_dec (fun x => terms x -> term)). hyp. subst f0. rewrite sub_fun. apply f_equal with (f := Fun f). set (s := fsub m v0). set (v1 := fresh (S m) (sum cs)). assert (Vmap (sub s) (Vmap_sum cs v1) = Vmap_sum cs (Vmap (sub s) v1)). unfold cs. eapply Vmap_map_sum with (m := m). unfold s. apply fsub_inf. apply Nat.le_refl. rewrite H4. assert (Vmap (sub s) v1 = conc cs). unfold s, v1. rewrite H3, Vmap_fsub_fresh. refl. rewrite H5. unfold cs. apply Vmap_sum_conc. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)