Update src/abs.ott

Co-authored-by: Karl Palmskog <palmskog@gmail.com>
kth-step · Jan 23, 2024 · 3c436f2 · 3c436f2
1 parent a11b9d5
commit 3c436f2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/abs.ott b/src/abs.ott
@@ -147,7 +147,7 @@ Lemma size_ge_1: forall e0,
      1 <= e_size e0.
 Proof. destruct e0;cbn;lia. Qed.
 
-Program Fixpoint my_fresh (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
+Program Fixpoint fresh_vars (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
   match e0 with
   | e_t _ => True
   | e_var x => ~ In x l