fact: Fixpoint subst (a: term) (x: string) (c: term) : term := match a with | Var y => if string_dec x y then c else Var y | Abs y a => if string_dec x y then Abs y a else Abs y (subst a x c) | App a1 a2 => App (subst a1 x c) (subst a2 x c) | Const b => Const b | Cond a ifso ifnot => Cond (subst a x c) (subst ifso x c) (subst ifnot x c) end.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)