proposition: Lemma subst_open_rec_c : forall e1 e2 u (x : atom) k, lc_c u -> [x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
proof: Proof. Admitted. Lemma subst_open_var_c : forall (x y : atom) u e, y <> x -> lc_c u -> open ([x ~> u] e) y = [x ~> u] (open e y). Proof. Admitted. Lemma subst_lc_c : forall (x : atom) u e, lc_c e -> lc_c u -> lc_c ([x ~> u] e). Proof. intros x u e He Hu. induction He. Case "lc_var_c". simpl. destruct (x0 == x). auto. auto. Case "lc_abs_c". simpl. Admitted. End CofiniteQuantification. Ltac gather_atoms ::= let A := gather_atoms_with (fun x : atoms => x) in let B := gather_atoms_with (fun x : atom => singleton x) in let C := gather_atoms_with (fun x : list (atom * typ) => dom x) in let D := gather_atoms_with (fun x : exp => fv x) in constr:(A `union` B `union` C `union` D). Lemma subst_lc_c_alternate_proof : forall (x : atom) u e, lc_c e -> lc_c u -> lc_c ([x ~> u] e). Proof. intros x u e He Hu. induction He. Case "fvar". simpl. destruct (x0 == x). auto. auto. Case "abs". simpl. pick fresh y and apply lc_abs_c. rewrite subst_open_var_c. auto. auto. auto. Case "app". simpl. auto. Qed.
imports: Metalib.Metatheory String