diff --git a/docsrc/examples/eter-semantics/from-fix.txt b/docsrc/examples/eter-semantics/from-fix.txt
new file mode 100644
index 0000000..732f553
--- /dev/null
+++ b/docsrc/examples/eter-semantics/from-fix.txt
@@ -0,0 +1,761 @@
+// ========================================================================
+// ========================================================================
+// SCALAR TYPES
+// ========================================================================
+// ========================================================================
+
+
+// ==========
+// Imm to Imm
+// ==========
+fn f(imm x: i32) {}
+fn main() {
+    let imm x: i32 = 1;
+    let imm y: i32 = x;
+    f(x);
+}
+
+// ==========
+// Imm to Mut
+// ==========
+fn f(mut x: i32) {}
+fn main() {
+    let imm x: i32 = 1;
+    // let mut y: i32 = x; // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+    // f(x); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+// ===========
+// Imm to Proj
+// ===========
+fn f(proj x: i32) {}
+fn main() {
+    let x: i32 = 1;
+    // let proj y: i32 = &x; // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+    // f(&x); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+// ========================================================================
+// ========================================================================
+// ARRAY TYPES
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Imm to Imm
+// ==========
+fn f(imm x: [i32; 3]) {}
+fn main() {
+    let imm x: [i32; 3] = [1, 2, 3];
+    let imm y: [i32; 3] = x; // O(1)
+    f(x); // O(1)
+}
+
+// ==========
+// Imm to Mut
+// ==========
+fn f(mut x: [i32; 3]) {}
+fn main() {
+    let imm x: [i32; 3] = [1, 2, 3];
+    // let mut y: [i32; 3] = x; // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+    // f(x); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+// ===========
+// Imm to Proj
+// ===========
+fn f(proj x: [i32; 3]) {}
+fn main() {
+    let imm x: [i32; 3] = [1, 2, 3];
+    // let proj y: [i32; 3] = &x; // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+    // f(&x); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+// ========================================================================
+// ========================================================================
+// Structs with Imm
+// ========================================================================
+// ========================================================================
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+// ==========
+// Imm to Imm
+// ==========
+fn f(imm p: Point) {} // Drop(p)
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    let imm q = p;
+    f(p);
+} // Drop(q), Drop(p)
+
+// ==========
+// Imm to Mut
+// ==========
+fn f(mut p: Point) {} // Drop(p)
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let mut q = p; // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+    // f(p); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+// ===========
+// Imm to Proj
+// ===========
+fn f(proj p: Point) {} // (proj parameter, no Drop)
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let proj q = &p; // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+    // f(&p); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+// ========================================================================
+// ========================================================================
+// Imm-Imm as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Imm-Imm to Imm
+// ==========
+fn imm f(imm p: Point): Point { p }
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    let imm q = f(p);
+} // Drop(q), Drop(p)
+
+fn imm f2(imm p1: Point, imm p2: Point): Point { p1 } // Drop(p2)
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);
+} // Drop(q), Drop(p1), Drop(p2)
+
+// ==========
+// Imm-Imm to Mut
+// ==========
+fn imm f(imm p: Point): Point { p } // p is returned, no Drop
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let mut q = f(p); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+fn imm f2(imm p1: Point, imm p2: Point): Point { p1 } // Drop(p2)
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    // let mut q = f2(p1, p2); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+// ===========
+// Imm-Imm to Proj
+// ===========
+fn imm f(imm p: Point): Point { p } // p is returned, no Drop
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let proj q = &f(p); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+fn imm f2(imm p1: Point, imm p2: Point): Point { p1 } // Drop(p2)
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    // let proj q = &f2(p1, p2); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+// ========================================================================
+// ========================================================================
+// Imm-Mut as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Imm-Mut to Imm
+// ==========
+fn imm f(mut p: Point): Point { p } // p is moved to return, no Drop
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let imm q = f(p);
+} // Drop(q) (p was moved, so no Drop for p)
+
+fn imm f2(mut p1: Point, mut p2: Point): Point { p1 } // p2 is dropped (p1 is returned)
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);
+} // Drop(q) (p1, p2 were moved)
+
+// ==========
+// Imm-Mut to Mut
+// ==========
+fn imm f(mut p: Point): Point { p } // p is moved to return, no Drop
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    // let mut q = f(p); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+fn imm f2(mut p1: Point, mut p2: Point): Point { p1 } // Drop(p2)
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    // let mut q = f2(p1, p2); // ERROR: Changing the regime from imm to mut is not allowed. Need to copy.
+}
+
+// ===========
+// Imm-Mut to Proj
+// ===========
+fn imm f(mut p: Point): Point { p } // p is moved to return, no Drop
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    // let proj q = &f(p); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+fn imm f2(mut p1: Point, mut p2: Point): Point { p1 } // Drop(p2)
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    // let proj q = &f2(p1, p2); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+// ========================================================================
+// ========================================================================
+// Imm-Proj as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+
+// ==========
+// Imm-Proj to Imm
+// ==========
+fn imm f(proj p: Point): Point {
+    // p // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let imm q = f(&p);
+}
+
+fn imm f2(proj p1: Point, proj p2: Point): Point {
+    // p1 // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 }
+    let proj p2 = &Point { x: 3, y: 4 };
+    let imm q = f2(&p1, &p2);
+}
+
+// ==========
+// Imm-Proj to Mut
+// ==========
+fn imm f(proj p: Point): Point {
+    // p // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let imm q = f(&p);
+}
+
+fn imm f2(proj p1: Point, proj p2: Point): Point {
+    p1 // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let imm q = f2(&p1, &p2);
+}
+
+// ===========
+// Imm-Proj to Proj
+// ===========
+fn imm f(proj p: Point): Point {
+    // p // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    // let proj q = &f(&p); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+fn imm f2(proj p1: Point, proj p2: Point): Point {
+    // p1 // ERROR: Escaping the return of a proj to a imm is not allowed. Need to copy.
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    // let proj q = &f2(&p1, &p2); // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+
+
+// ========================================================================
+// ========================================================================
+// Store Imm in Struct from Imm
+// ========================================================================
+// ========================================================================
+
+// ==========
+// SINGLE CASE
+// ==========
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn imm f(imm p: Point): Point {
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+} // Drop(p)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = f(p1);
+} // Drop(p2), Drop(p1)
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let imm p2;
+//     let tmp = Point { x: 1, y: 2 };
+//     {
+//         let p1 = tmp;
+//         p2 = f(p1);
+//     }
+// }
+fn tmp2() {
+    let imm p2;
+    {
+        let imm p1 = Point { x: 1, y: 2 };
+        p2 = f(p1);
+    } // Drop(p1)
+} // Drop(p2)
+
+// ==========
+// Imm-Imm-Imm as return and formal parameters from Imm
+// =========
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn imm f(imm p: Point, imm u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let imm p2 = f(p1, p2);
+} // Drop(p1), Drop(p2_shadowed), Drop(p2)
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let p2;
+//     let p = Point { x: 1, y: 2 };
+//     let tmp = Point { x: 3, y: 4 };
+//     {
+//         let u = tmp;
+//         p2 = f(p, tmp);
+//     }
+// }
+fn tmp2() {
+    let imm p2;
+    let imm p = Point { x: 1, y: 2 };
+    {
+        let imm u = Point { x: 3, y: 4 };
+        p2 = f(p, u);
+    } // Drop(u)
+} // Drop(p2), Drop(p)
+
+
+
+// ==========
+// Imm-Imm-Mut as return and formal parameters from Imm
+// =========
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn imm f(imm p: Point, mut u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, p2);
+    // - p2 is moved, so it is not used anymore
+    // - p1 can be used again
+} // Drop(p3), Drop(p1) (p2 moved into f)
+
+
+// OPTIMIZATION to avoid copy and reference counting
+// fn tmp2() {
+//     let p3;
+//     let p1 = Point { x: 1, y: 2 };
+//     let mut tmp = Point { x: 3, y: 4 };
+//     {
+//         let mut p2 = tmp;
+//         p3 = f(p1, p2);
+//     }
+// }
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p2 is moved, so it is not used anymore
+        // - p1 can be used again
+    } // (p2 moved into f, no Drop at inner scope)
+} // Drop(p3), Drop(p1)
+
+// ==========
+// Imm-Imm-Proj as return and formal parameters from Imm
+// =========
+
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn imm f(imm p: Point, proj u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    *p.x = 10; // Re-initialize the projection.
+    *p.y = 20; // Re-initialize the projection.
+    Point { x, y }
+} // Drop(p) (u is proj, no Drop)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, &p2);
+    // - p2 is projected, so it is can be used again
+    // - p1 can be used again
+} // Drop(p3), Drop(p2), Drop(p1)
+
+
+// OPTIMIZATION to avoid copy and reference counting
+// fn tmp2() {
+//     let p3;
+//     let p1 = Point { x: 1, y: 2 };
+//     let mut tmp = Point { x: 3, y: 4 };
+//     {
+//         let mut p2 = tmp;
+//         p3 = f(p1, p2);
+//     }
+// }
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p2 is projected, so it is can be used again
+        // - p1 can be used again
+    } // Drop(p2) (p2 was projected, not moved)
+} // Drop(p3), Drop(p1)
+
+// ========================================================================
+// ========================================================================
+// Store Mut in Struct from Imm
+// ========================================================================
+// ========================================================================
+
+// ==========
+// SINGLE CASE
+// ==========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn imm f(imm p: Point): Point {
+    // let mut x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let mut y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = f(p1);
+} // Drop(p2), Drop(p1)
+
+fn tmp2() {
+    let imm p2;
+    {
+        let imm p1 = Point { x: 1, y: 2 };
+        p2 = f(p1);
+    } // Drop(p1)
+} // Drop(p2)
+
+// ==========
+// Imm-Imm-Imm as return and formal parameters from Imm
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn imm f(imm p: Point, imm u: Point): Point {
+    // u is not used
+    // let mut x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let mut y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let imm p2 = f(p1, p2);
+} // Drop(p1), Drop(p2_shadowed), Drop(p2)
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let p2;
+//     let p = Point { x: 1, y: 2 };
+//     let tmp = Point { x: 3, y: 4 };
+//     {
+//         let u = tmp;
+//         p2 = f(p, tmp);
+//     }
+// }
+fn tmp2() {
+    let imm p2;
+    let imm p = Point { x: 1, y: 2 };
+    {
+        let imm u = Point { x: 3, y: 4 };
+        p2 = f(p, u);
+    } // Drop(u)
+} // Drop(p2), Drop(p)
+
+// ==========
+// Imm-Imm-Mut as return and formal parameters from Imm
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn imm f(imm p: Point, mut u: Point): Point {
+    // u is not used
+    // let mut x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let mut y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, p2);
+    // - p2 is moved, so it is not used anymore
+    // - p1 can be used again
+} // Drop(p3), Drop(p1) (p2 moved into f)
+
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p2 is moved, so it is not used anymore
+        // - p1 can be used again
+    } // (p2 moved into f, no Drop at inner scope)
+} // Drop(p3), Drop(p1)
+
+// ==========
+// Imm-Imm-Proj as return and formal parameters from Imm
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn imm f(imm p: Point, proj u: Point): Point {
+    // u is not used
+    // let mut x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let mut y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p) (u is proj, no Drop)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, &p2);
+    // - p2 is projected, so it is can be used again
+    // - p1 can be used again
+} // Drop(p3), Drop(p2), Drop(p1)
+
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p2 is projected, so it is can be used again
+        // - p1 can be used again
+    } // Drop(p2) (p2 was projected, not moved)
+} // Drop(p3), Drop(p1)
+
+// ========================================================================
+// ========================================================================
+// Store Proj in Struct from Imm
+// ========================================================================
+// ========================================================================
+
+// ==========
+// SINGLE CASE
+// ==========
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn imm f(imm p: Point): Point {
+    // let proj x = &p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let proj y = &p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p)
+
+fn tmp1() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = f(&p1);
+} // (proj variables, no Drop)
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let p2;
+//     let p = Point { x: 1, y: 2 };
+//     let tmp = Point { x: 3, y: 4 };
+//     {
+//         let u = tmp;
+//         p2 = f(p);
+//     }
+// }
+fn tmp2() {
+    let proj p2;
+    let proj p = Point { x: 1, y: 2 };
+    {
+        let proj u = Point { x: 3, y: 4 };
+        p2 = f(p);
+    } // (proj variables, no Drop)
+} // (proj variables, no Drop)
+
+// ==========
+// Imm-Imm-Imm as return and formal parameters from Imm
+// =========
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn imm f(imm p: Point, imm u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let proj y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let imm p2 = f(p1, p2);
+} // Drop(p1), Drop(p2_shadowed), Drop(p2)
+
+fn tmp2() {
+    let imm p2;
+    let imm p = Point { x: 1, y: 2 };
+    {
+        let imm u = Point { x: 3, y: 4 };
+        p2 = f(p, u);
+    } // Drop(u)
+} // Drop(p2), Drop(p)
+
+// ==========
+// Imm-Imm-Mut as return and formal parameters from Imm
+// =========
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn imm f(imm p: Point, mut u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let proj y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p), Drop(u)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, p2);
+    // - p2 is moved, so it is not used anymore
+    // - p1 can be used again
+} // Drop(p3), Drop(p1) (p2 moved into f)
+
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p2 is moved, so it is not used anymore
+        // - p1 can be used again
+    } // (p2 moved into f, no Drop at inner scope)
+} // Drop(p3), Drop(p1)
+
+// ==========
+// Imm-Imm-Proj as return and formal parameters from Imm
+// =========
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn imm f(imm p: Point, proj u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    // let proj y = p.y; // ERROR: p is under the regime imm, it propagates to the whole struct.
+    Point { x, y }
+} // Drop(p) (u is proj, no Drop)
+
+fn tmp1() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let imm p3 = f(p1, &p2);
+    // - p2 is projected, so it is can be used again
+    // - p1 can be used again
+} // Drop(p3), Drop(p2), Drop(p1)
+
+fn tmp2() {
+    let imm p3;
+    let imm p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p2 is projected, so it is can be used again
+        // - p1 can be used again
+    } // Drop(p2) (p2 was projected, not moved)
+} // Drop(p3), Drop(p1)
\ No newline at end of file
diff --git a/docsrc/examples/eter-semantics/from-mut.txt b/docsrc/examples/eter-semantics/from-mut.txt
new file mode 100644
index 0000000..10d36a5
--- /dev/null
+++ b/docsrc/examples/eter-semantics/from-mut.txt
@@ -0,0 +1,872 @@
+// ========================================================================
+// ========================================================================
+// SCALAR TYPES
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Mut to Mut
+// ==========
+fn main() {
+    let mut x: i32 = 1;
+    let mut y: i32 = x;
+    // let mut z: i32 = x; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+fn f(mut x: i32) {}
+fn main() {
+    let mut x: i32 = 1;
+    f(x);
+    // let mut z: i32 = x; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+// ==========
+// Mut to Imm
+// ==========
+fn main() {
+    let mut x: i32 = 1;
+    let imm y: i32 = x;
+    let imm z: i32 = x;
+    // let mut z: i32 = x; // ERROR: `x` is has been moved, so it is not valid to use it again.
+}
+
+fn f(imm x: i32) {}
+fn main() {
+    let mut x: i32 = 1;
+    f(x);
+    let imm z: i32 = x;
+    // let mut z: i32 = x; // ERROR: `x` is has been moved, so it is not valid to use it again.
+}
+
+// ===========
+// Mut to Proj
+// ===========
+fn main() {
+    let mut x: i32 = 1;
+    let proj y: i32 = &x;
+    // let proj z: i32 = &x; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    *y = 2;
+    // NOTE: x can be eventually used again if y is not used anymore.
+}
+
+fn f(proj x: i32) {}
+fn main() {
+    let mut x: i32 = 1;
+    f(&x);
+    // let proj y: i32 = &x; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    &x = 2;
+    // NOTE: x can be eventually used again.
+}
+
+// ========================================================================
+// ========================================================================
+// ARRAY TYPES
+// ========================================================================
+// ========================================================================
+
+
+// ==========
+// Mut to Mut
+// ==========
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    let mut y: [i32; 3] = x;
+    // let mut z: [i32; 3] = x; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+fn f(mut x: [i32; 3]) {}
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    f(x);
+    // let mut z: [i32; 3] = x; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+// ==========
+// Mut to Imm
+// ==========
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    let imm y: [i32; 3] = x;
+    let imm z: [i32; 3] = x;
+}
+
+fn f(imm x: [i32; 3]) {}
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    f(x);
+    let imm z: [i32; 3] = x;
+}
+
+// ===========
+// Mut to Proj
+// ===========
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    let proj y: [i32; 3] = &x;
+    // let proj z: [i32; 3] = &x; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    *y = [3, 2, 1];
+    // NOTE: x can be eventually used again if y is not used anymore.
+}
+
+fn f(proj x: [i32; 3]) {}
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    f(&x);
+    // let proj y: [i32; 3] = &x; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    *y = [3, 2, 1];
+    // NOTE: x can be eventually used again if y is not used anymore.
+}
+
+// ========================================================================
+// ========================================================================
+// Structs with Imm
+// ========================================================================
+// ========================================================================
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+// ==========
+// Mut to Mut
+// ==========
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let mut q = p;
+    // let mut r = p; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+fn f(mut p: Point) {}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    f(p);
+    // let mut r = p; // ERROR: Changing the regime from mut to mut is allowed only once. Need to copy.
+}
+
+// ==========
+// Mut to Imm
+// ==========
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let imm q = p;
+    let imm r = p;
+    // let mut z: i32 = x; // ERROR: `x` is has been moved, so it is not valid to use it again.
+}
+
+fn f(imm p: Point) {}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    f(p);
+    let imm r = p;
+}
+
+// ===========
+// Mut to Proj
+// ===========
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let proj q = &p;
+    // let proj r = &p; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    *q = Point { x: 3, y: 4 };
+    // NOTE: p can be eventually used again if q is not used anymore.
+}
+
+fn f(proj p: Point) {}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    f(&p);
+    // let proj q = &p; // ERROR: Changing the regime from mut to proj is allowed only once. Need to copy.
+    // NOTE: p can be eventually used again.
+}
+
+// ========================================================================
+// ========================================================================
+// Mut-Mut as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Mut-Mut to Mut
+// ==========
+fn mut f(mut p: Point): Point { p }
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let mut q = f(p);
+}
+
+fn mut f2(mut p1: Point, mut p2: Point): Point { p1 }
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut q = f2(p1, p2);
+    // - p2 is moved, so it is not used anymore
+    // - p1 is moved, so it is not used anymore
+}
+
+// ==========
+// Mut-Mut to Imm
+// ==========
+fn mut f(mut p: Point): Point { p }
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let imm q = f(p);
+}
+
+fn mut f2(mut p1: Point, mut p2: Point): Point { p1 }
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);
+}
+
+// ===========
+// Mut-Mut to Proj
+// ===========
+fn mut f(mut p: Point): Point { p }
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    let proj q = &f(p);
+}
+
+fn mut f2(mut p1: Point, mut p2: Point): Point { p1 }
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let proj q = &f2(p1, p2);
+}
+
+// ========================================================================
+// ========================================================================
+// Mut-Imm as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Mut-Imm to Mut
+// ==========
+fn mut f(imm p: Point): Point {
+    // p // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    let mut q = f(p);
+}
+
+fn mut f2(imm p1: Point, imm p2: Point): Point {
+    // p1 // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let mut q = f2(p1, p2);
+}
+
+// ==========
+// Mut-Imm to Imm
+// ==========
+fn mut f(imm p: Point): Point {
+    // p // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    let imm q = f(p);
+}
+
+fn mut f2(imm p1: Point, imm p2: Point): Point {
+    // p1  // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);
+}
+
+// ==========
+// Mut-Imm to Proj
+// ==========
+fn mut f(imm p: Point): Point {
+    // p // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    let proj q = f(p);
+}
+
+fn mut f2(imm p1: Point, imm p2: Point): Point {
+    // p1  // ERROR: Escaping the return of a imm to a mut is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let proj q = f2(p1, p2);
+}
+
+// ========================================================================
+// ========================================================================
+// Mut-Proj as return and formal parameter
+// ========================================================================
+// ========================================================================
+
+// NOTE: When calling fn mut f(proj p), p must be forwarded (not aliased).
+// If p is already a proj binding, f(p) is OK (forwarding, p is consumed).
+// f(&p) where p is already proj is ERROR (aliasing — two projs to same location).
+
+// ==========
+// Mut-Proj to Mut
+// ==========
+fn mut f(proj p: Point): Point {
+    let imm x = p.x;  // proj binding + imm field -> imm access
+    let imm y = p.y;
+    Point { x, y }    // OK: returning a new mut value
+    // p // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let mut q = f(p);   // OK: forwarding — p is consumed, q holds new mut value
+    // f(&p);           // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn mut f2(proj p1: Point, proj p2: Point): Point {
+    let imm x = p1.x;
+    let imm y = p1.y;
+    Point { x, y }    // p2 unused but consumed as proj param
+    // p1 // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let mut q = f2(p1, p2);   // OK: both forwarded
+    // f2(&p1, &p2);           // ERROR: aliasing — &p1, &p2 create new projs while originals alive
+}
+
+// ==========
+// Mut-Proj to Imm
+// ==========
+fn mut f(proj p: Point): Point {
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+    // p // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let imm q = f(p);   // OK: forwarding, then mut -> imm at call site
+    // f(&p);           // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn mut f2(proj p1: Point, proj p2: Point): Point {
+    let imm x = p1.x;
+    let imm y = p1.y;
+    Point { x, y }
+    // p1 // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);    // OK: both forwarded
+    // f2(&p1, &p2);            // ERROR: aliasing
+}
+
+// ==========
+// Mut-Proj to Proj
+// ==========
+fn mut f(proj p: Point): Point {
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+    // p // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let proj q = &f(p);  // OK: forwarding p, then proj of the returned mut value
+    // f(&p);            // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn mut f2(proj p1: Point, proj p2: Point): Point {
+    let imm x = p1.x;
+    let imm y = p1.y;
+    Point { x, y }
+    // p1 // ERROR: returning proj directly escapes the projection
+}
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let proj q = &f2(p1, p2);  // OK: both forwarded, then proj of returned mut value
+    // f2(&p1, &p2);            // ERROR: aliasing
+}
+
+
+// ========================================================================
+// ========================================================================
+// Store Mut in Struct from Mut
+// ========================================================================
+// ========================================================================
+
+// ==========
+// SINGLE CASE
+// ==========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(mut p: Point): Point {
+    let mut x = p.x;
+    let mut y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = f(p1);
+    // - p1 is moved, so it is not used anymore
+}
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let mut p2;
+//     let mut tmp = Point { x: 1, y: 2 };
+//     {
+//         let mut p1 = tmp;
+//         p2 = f(p1);
+//     }
+// }
+fn tmp2() {
+    let mut p2;
+    {
+        let mut p1 = Point { x: 1, y: 2 };
+        p2 = f(p1);
+    }
+}
+
+// ==========
+// Mut-Mut-Mut as return and formal parameters fromMut
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(mut p: Point, mut : Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p2 = f(p1, p2);
+}
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let mut p2;
+//     let mut p = Point { x: 1, y: 2 };
+//     let mut tmp = Point { x: 3, y: 4 };
+//     {
+//         let mut u = tmp;
+//         p2 = f(p, tmp);
+//     }
+// }
+fn tmp2() {
+    let mut p2;
+    let mut p = Point { x: 1, y: 2 };
+    {
+        let mut u = Point { x: 3, y: 4 };
+        p2 = f(p, u);
+    }
+}
+
+
+// ==========
+// Mut-Mut-Imm as return and formal parameters fromMut
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(mut p: Point, imm u: Point): Point {
+    // u is not used
+    let mut x = p.x;
+    let mut y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 1, y: 2 };
+    let mut p3 = f(p1, p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 can be used again
+}
+
+
+// OPTIMIZATION to avoid copy and reference counting
+// fn tmp2() {
+//     let mut p3;
+//     let mut p1 = Point { x: 1, y: 2 };
+//     let tmp = Point { x: 3, y: 4 };
+//     {
+//         let p2 = tmp;
+//         p3 = f(p1, p2);
+//     }
+// }
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p1 is moved, so it is not used anymore
+        // - p2 can be used again
+    }
+}
+
+
+
+// ==========
+// Mut-Mut-Proj as return and formal parameters fromMut
+// =========
+
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(mut p: Point, proj u: Point): Point {
+    // u is not used
+    let mut x = p.x;
+    let mut y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let mut p3 = f(p1, &p2);
+    // - p2 is projected, so it is can be used again
+    // - p1 is moved, so it is not used anymore
+}
+
+
+// OPTIMIZATION to avoid copy and reference counting
+// fn tmp2() {
+//     let mut p3;
+//     let mut p1 = Point { x: 1, y: 2 };
+//     let mut tmp = Point { x: 3, y: 4 };
+//     {
+//         let mut p2 = tmp;
+//         p3 = f(p1, p2);
+//     }
+// }
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p2 is projected, so it is can be used again
+        // - p1 is moved, so it is not used anymore
+    }
+}
+
+// ========================================================================
+// ========================================================================
+// Store Proj in Struct from Mut
+// ========================================================================
+// ========================================================================
+
+// ==========
+// SINGLE CASE
+// ==========
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn mut f(mut p: Point): Point {
+    let mut x = p.x; // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    let mut y = p.y; // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    &p.x = 10;
+    &p.y = 20;
+    // Point { x, y } creates a new Point that OWNS x and y.
+    // The `proj` field marker describes the access mode (in-place mutable reference),
+    // not external storage — the struct owns its data.
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = f(p1);
+}
+
+// OPTIMIZATION: to avoid copy and reference counting
+// fn tmp2() {
+//     let mut p2;
+//     let mut tmp = Point { x: 1, y: 2 };
+//     {
+//         let mut p1 = tmp;
+//         p2 = f(p1);
+//     }
+// }
+fn tmp2() {
+    let mut p2;
+    {
+        let mut p1 = Point { x: 1, y: 2 };
+        p2 = f(p1);
+    }
+}
+
+// ==========
+// Mut-Mut-Mut as return and formal parameters fromMut
+// =========
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn mut f(mut p: Point, mut u: Point): Point {
+    // u is not used
+    let mut x = p.x; // NOTE: proj -> mut forces reinitialization
+    let mut y = p.y; // NOTE: proj -> mut forces reinitialization
+    &p.x = 10;
+    &p.y = 20;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 is moved, so it is not used anymore
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+    }
+}
+
+// ==========
+// Mut-Mut-Imm as return and formal parameters fromMut
+// =========
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn mut f(mut p: Point, imm u: Point): Point {
+    // u is not used
+    let mut x = p.x; // NOTE: proj -> mut forces reinitialization
+    let mut y = p.y; // NOTE: proj -> mut forces reinitialization
+    &p.x = 10;
+    &p.y = 20;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 can be used again
+}
+
+// OPTIMIZATION to avoid copy and reference counting
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p1 is moved, so it is not used anymore
+        // - p2 can be used again
+    }
+}
+
+// ==========
+// Mut-Mut-Proj as return and formal parameters fromMut
+// =========
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn mut f(mut p: Point, proj u: Point): Point {
+    // u is not used
+    let mut x = p.x; // NOTE: proj -> mut forces reinitialization
+    let mut y = p.y; // NOTE: proj -> mut forces reinitialization
+    &p.x = 10;
+    &p.y = 20;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, &p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 is projected, so it can be used again
+}
+
+// OPTIMIZATION to avoid copy and reference counting
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p1 is moved, so it is not used anymore
+        // - p2 is projected, so it can be used again
+    }
+}
+
+// ========================================================================
+// ========================================================================
+// Store Imm in Struct from Mut
+// ========================================================================
+// ========================================================================
+
+
+// ==========
+// SINGLE CASE
+// ==========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(mut p: Point): Point {
+    let imm x = p.x; // imm fields are always imm, even under mut binding
+    let imm y = p.y;
+    // let mut x = p.x; // ERROR: imm fields cannot be accessed as mut. Need to copy.
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = f(p1);
+    // - p1 is moved, so it is not used anymore
+}
+
+// OPTIMIZATION: to avoid copy and reference counting
+fn tmp2() {
+    let mut p2;
+    {
+        let mut p1 = Point { x: 1, y: 2 };
+        p2 = f(p1);
+    }
+}
+
+// ==========
+// Mut-Mut-Mut as return and formal parameters fromMut
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(mut p: Point, mut u: Point): Point {
+    // u is not used
+    let imm x = p.x; // imm fields are always imm
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 is moved, so it is not used anymore
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+    }
+}
+
+// ==========
+// Mut-Mut-Imm as return and formal parameters fromMut
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(mut p: Point, imm u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 can be used again
+}
+
+// OPTIMIZATION to avoid copy and reference counting
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);
+        // - p1 is moved, so it is not used anymore
+        // - p2 can be used again
+    }
+}
+
+// ==========
+// Mut-Mut-Proj as return and formal parameters fromMut
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(mut p: Point, proj u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(p1, &p2);
+    // - p1 is moved, so it is not used anymore
+    // - p2 is projected, so it can be used again
+}
+
+// OPTIMIZATION to avoid copy and reference counting
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, &p2);
+        // - p1 is moved, so it is not used anymore
+        // - p2 is projected, so it can be used again
+    }
+}
diff --git a/docsrc/examples/eter-semantics/from-proj.txt b/docsrc/examples/eter-semantics/from-proj.txt
new file mode 100644
index 0000000..dd87117
--- /dev/null
+++ b/docsrc/examples/eter-semantics/from-proj.txt
@@ -0,0 +1,808 @@
+// ========================================================================
+// ========================================================================
+// SCALAR TYPES
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Proj to Proj
+// ==========
+
+fn main() {
+    let proj x: i32 = &1;
+    let proj y: i32 = x;     // OK: forwarding (x is consumed, x is dead after this)
+    // let proj z: i32 = &x; // ERROR: aliasing — cannot create a new proj while x is still alive
+}
+
+fn f(proj x: i32) {}
+fn main() {
+    let proj x: i32 = &1;
+    f(x);    // OK: forwarding x to f (x is consumed during the call)
+    // f(&x); // ERROR: aliasing — &x creates a new proj while x is still alive
+}
+
+// ==========
+// Proj to Imm
+// ==========
+
+fn main() {
+    let proj x: i32 = &1;
+    let imm y: i32 = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm z: i32 = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    x = &2; // NOTE: Reinitialization is not always needed.
+}
+
+fn f(imm x: i32) {}
+fn main() {
+    let proj x: i32 = &1;
+    f(x);               // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm z: i32 = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    x = &2; // NOTE: Reinitialization is not always needed.
+}
+
+// ==========
+// Proj to Mut
+// ==========
+
+fn main() {
+    let proj x: i32 = &1;
+    let mut y: i32 = x; // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut z: i32 = x; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                           //        This is to guarantee both that only one mutation is active at a time.
+    x = &2; // NOTE: Reinitialization is not always needed.
+}
+
+// OPTIMIZATION2
+fn f(mut x: i32) {}
+fn main() {
+    let proj x: i32 = &1;
+    f(x); // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut z: i32 = x; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                           //        This is to guarantee both that only one mutation is active at a time.
+    x = &2; // NOTE: Reinitialization is not always needed.
+}
+
+// ========================================================================
+// ========================================================================
+// ARRAY TYPES
+// ========================================================================
+// ========================================================================
+
+// ==========
+// Proj to Proj
+// ==========
+
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    let proj y: [i32; 3] = x;     // OK: forwarding (x is consumed, x is dead after this)
+    // let proj z: [i32; 3] = &x; // ERROR: aliasing — cannot create a new proj while x is still alive
+}
+
+fn f(proj x: [i32; 3]) {}
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    f(x);    // OK: forwarding x to f (x is consumed during the call)
+    // f(&x); // ERROR: aliasing — &x creates a new proj while x is still alive
+}
+
+// ==========
+// Proj to Imm
+// ==========
+
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    let imm y: [i32; 3] = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm z: [i32; 3] = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    x = &[3, 2, 1]; // NOTE: Reinitialization is not always needed.
+}
+
+fn f(imm x: [i32; 3]) {}
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    f(x);                    // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm z: [i32; 3] = x; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    x = &[3, 2, 1]; // NOTE: Reinitialization is not always needed.
+}
+
+// ==========
+// Proj to Mut
+// ==========
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    let mut y: [i32; 3] = x; // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut z: [i32; 3] = x; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                               //        This is to guarantee both that only one mutation is active at a time.
+    x = &[3, 2, 1]; // NOTE: Reinitialization is not always needed.
+}
+
+fn f(mut x: [i32; 3]) {}
+fn main() {
+    let proj x: [i32; 3] = &[1, 2, 3];
+    f(x); // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut z: [i32; 3] = x; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                               //        This is to guarantee both that only one mutation is active at a time.
+    x = &[3, 2, 1]; // NOTE: Reinitialization is not always needed.
+}
+
+// ========================================================================
+// ========================================================================
+// Structs with Imm
+// ========================================================================
+// ========================================================================
+
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+// ==========
+// Proj to Proj
+// ==========
+
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let proj q = p;     // OK: forwarding (p is consumed, p is dead after this)
+    // let proj r = &p; // ERROR: aliasing — cannot create a new proj while p is still alive
+}
+
+fn f(proj p: Point) {}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    f(p);    // OK: forwarding p to f (p is consumed during the call)
+    // f(&p); // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+// ==========
+// Proj to Imm
+// ==========
+
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let imm q = p; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm r = p; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    p = &Point { x: 3, y: 4 }; // NOTE: Reinitialization is not always needed.
+}
+
+fn f(imm p: Point) {}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    f(p);          // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    let imm q = p; // NOTE: Changing the regime from proj to imm forces a reinitialization of the projection.
+    p = &Point { x: 3, y: 4 }; // NOTE: Reinitialization is not always needed.
+}
+
+// ==========
+// Proj to Mut
+// ==========
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let mut q = p; // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut r = p; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                     //        This is to guarantee both that only one mutation is active at a time.
+    p = &Point { x: 3, y: 4 }; // NOTE: Reinitialization is not always needed.
+}
+
+fn f(mut p: Point) {}
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    f(p); // NOTE: Changing the regime from proj to mut forces a reinitialization of the projection.
+    // let mut r = p; // ERROR: Changing the regime from proj to mut is allowed only once. Need to copy.
+                     //        This is to guarantee both that only one mutation is active at a time.
+    p = &Point { x: 3, y: 4 }; // NOTE: Reinitialization is not always needed.
+}
+
+// ========================================================================
+// ========================================================================
+// Proj-Proj as Formal Parameter and Return
+// ========================================================================
+// ========================================================================
+
+// NOTE: Inside the body, `p` is already proj. Returning `p` forwards the proj (OK).
+// Returning `&p` would alias it (ERROR). At the call site, `f(p)` forwards (OK);
+// `f(&p)` would create a new proj while p is still alive (ERROR).
+
+// ==========
+// Proj-Proj to Proj
+// ==========
+
+fn proj f(proj p: Point): Point { p }  // OK: forwarding p as the proj return
+// fn proj f_bad(proj p: Point): Point { &p }  // ERROR: aliasing — &p while p is already proj
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let proj q = f(p);   // OK: forwarding — p is consumed, q holds the proj
+    // f(&p);            // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn proj f2(proj p1: Point, proj p2: Point): Point { p1 }  // OK: forwarding p1 (p2 unused but consumed)
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let proj q = f2(p1, p2);   // OK: both forwarded, q holds the proj that was p1
+    // f2(&p1, &p2);            // ERROR: aliasing — &p1, &p2 create new projs while originals alive
+}
+
+// ==========
+// Proj-Proj to Imm
+// ==========
+fn proj f(proj p: Point): Point { p }
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let imm q = f(p);   // OK: forwarding p, then proj -> imm (forced reinit of proj)
+    // f(&p);           // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn proj f2(proj p1: Point, proj p2: Point): Point { p1 }
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let imm q = f2(p1, p2);    // OK: forwarding, then proj -> imm
+    // f2(&p1, &p2);            // ERROR: aliasing
+}
+
+// ===========
+// Proj-Proj to Mut
+// ===========
+fn proj f(proj p: Point): Point { p }
+fn main() {
+    let proj p = &Point { x: 1, y: 2 };
+    let mut q = f(p);   // OK: forwarding p, then proj -> mut (forced reinit, allowed once)
+    // f(&p);           // ERROR: aliasing — &p creates a new proj while p is still alive
+}
+
+fn proj f2(proj p1: Point, proj p2: Point): Point { p1 }
+fn main() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 3, y: 4 };
+    let mut q = f2(p1, p2);    // OK: forwarding, then proj -> mut
+    // f2(&p1, &p2);            // ERROR: aliasing
+}
+
+// ========================================================================
+// ========================================================================
+// Proj-Imm as Formal Parameter and Return
+// ========================================================================
+// ========================================================================
+
+// NOTE: fn proj f(imm p) is a degenerate case.
+// A `imm` parameter cannot be projected (imm -> proj is forbidden),
+// so the function body cannot produce a valid proj return from its parameter.
+// All call-site usages are therefore also errors.
+
+// ==========
+// Proj-Imm to Imm
+// ==========
+fn proj f(imm p: Point): Point {
+    // &p // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let imm q = f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(imm p1: Point, imm p2: Point): Point {
+    // &p1 // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    // let imm q = f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ==========
+// Proj-Imm to Mut
+// ==========
+fn proj f(imm p: Point): Point {
+    // &p // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let mut q = f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(imm p1: Point, imm p2: Point): Point {
+    // &p1 // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    // let mut q = f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ===========
+// Proj-Imm to Proj
+// ===========
+fn proj f(imm p: Point): Point {
+    // &p // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p = Point { x: 1, y: 2 };
+    // let proj q = &f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(imm p1: Point, imm p2: Point): Point {
+    // &p1 // ERROR: Changing the regime from imm to proj is not allowed. Need to copy.
+}
+fn main() {
+    let imm p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    // let proj q = &f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ========================================================================
+// ========================================================================
+// Proj-Mut as Formal Parameter and Return
+// ========================================================================
+// ========================================================================
+
+// NOTE: fn proj f(mut p) is also a degenerate case.
+// A `mut` parameter is owned by the function (local binding).
+// Returning `&p` would create a proj to a local binding that escapes the function scope — dangling.
+// All call-site usages are therefore also errors.
+
+// ==========
+// Proj-Mut to Imm
+// ==========
+fn proj f(mut p: Point): Point {
+    // &p // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    // let imm q = f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(mut p1: Point, mut p2: Point): Point {
+    // &p1 // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    // let imm q = f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ==========
+// Proj-Mut to Mut
+// ==========
+fn proj f(mut p: Point): Point {
+    // &p // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    // let mut q = f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(mut p1: Point, mut p2: Point): Point {
+    // &p1 // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    // let mut q = f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ===========
+// Proj-Mut to Proj
+// ===========
+fn proj f(mut p: Point): Point {
+    // &p // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p = Point { x: 1, y: 2 };
+    // let proj q = &f(p); // ERROR: function body cannot produce a valid proj return
+}
+
+fn proj f2(mut p1: Point, mut p2: Point): Point {
+    // &p1 // ERROR: proj to local mut binding escapes function scope — dangling.
+}
+fn main() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    // let proj q = &f2(p1, p2); // ERROR: function body cannot produce a valid proj return
+}
+
+// ========================================================================
+// ========================================================================
+// Store Proj in Struct from Proj
+// ========================================================================
+// ========================================================================
+
+// NOTE: proj binding + proj field -> ERROR (would create aliased projections).
+// The only valid operation on a `proj` binding to a struct with proj fields is
+// forwarding the whole proj (consuming p and passing it along).
+
+// SINGLE CASE
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn proj f(proj p: Point): Point {
+    // let proj x = p.x; // ERROR: proj binding + proj field -> aliased projections forbidden
+    // let proj y = p.y; // ERROR: same
+    p  // OK: forwarding the entire proj (p is consumed)
+}
+
+fn tmp1() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = f(p1);  // OK: forwarding — p1 is consumed, p2 holds the proj
+    // f(&p1);            // ERROR: aliasing — &p1 creates a new proj while p1 is still alive
+}
+
+fn tmp2() {
+    let proj p2;
+    {
+        let proj p1 = &Point { x: 1, y: 2 };
+        p2 = f(p1);  // OK: forwarding
+    }
+}
+
+// ========================================================================
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn proj f(proj p: Point, proj u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: proj binding + proj field -> aliased projections forbidden
+    // let proj y = p.y; // ERROR: same
+    p  // OK: forwarding p (u is also consumed as unused proj param)
+}
+
+fn tmp1() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let proj p2 = &Point { x: 1, y: 2 };
+    let proj p3 = f(p1, p2);  // OK: both forwarded, p3 holds the proj that was p1
+    // f(&p1, &p2);            // ERROR: aliasing
+}
+
+fn tmp2() {
+    let proj p3;
+    let proj p1 = &Point { x: 1, y: 2 };
+    {
+        let proj p2 = &Point { x: 3, y: 4 };
+        p3 = f(p1, p2);  // OK: forwarding — both p1 and p2 consumed
+    }
+}
+
+// ========================================================================
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn proj f(proj p: Point, mut u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: proj binding + proj field -> aliased projections forbidden
+    // let proj y = p.y; // ERROR: same
+    p  // OK: forwarding p (u is consumed as owned mut param)
+}
+
+fn tmp1() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 1, y: 2 };
+    let proj p3 = f(p1, p2);  // OK: p1 forwarded, p2 moved (consumed)
+    // f(&p1, p2);             // ERROR: aliasing — &p1 creates a new proj while p1 alive
+}
+
+fn tmp2() {
+    let proj p3;
+    let proj p1 = &Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);  // OK: forwarding
+    }
+}
+
+// ========================================================================
+
+struct Point {
+    proj x: i32,
+    proj y: i32,
+}
+
+fn proj f(proj p: Point, imm u: Point): Point {
+    // u is not used
+    // let proj x = p.x; // ERROR: proj binding + proj field -> aliased projections forbidden
+    // let proj y = p.y; // ERROR: same
+    p  // OK: forwarding p (u is imm, shared immutable)
+}
+
+fn tmp1() {
+    let proj p1 = &Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 1, y: 2 };
+    let proj p3 = f(p1, p2);  // OK: p1 forwarded, p2 shared (imm can be passed many times)
+    // f(&p1, p2);             // ERROR: aliasing — &p1 creates a new proj while p1 alive
+}
+
+fn tmp2() {
+    let proj p3;
+    let proj p1 = &Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(p1, p2);  // OK: forwarding
+    }
+}
+
+// ========================================================================
+// ========================================================================
+// Store Mut in Struct from Proj
+// ========================================================================
+// ========================================================================
+
+// NOTE: proj binding + mut field -> proj access (in-place mutable reference to the field).
+// From a proj binding, accessing a mut field gives proj access to that field.
+
+// ==========
+// SINGLE CASE
+// ==========
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(proj p: Point): Point {
+    // p.x gives proj access (proj binding + mut field -> proj)
+    let mut x = p.x; // proj -> mut: allowed once, forces reinitialization of p.x
+    let mut y = p.y; // proj -> mut: allowed once, forces reinitialization of p.y
+    *p.x = 10;       // reinit p.x
+    *p.y = 20;       // reinit p.y
+    Point { x, y }   // OK: returning a new Point (not the projection itself)
+    // p // ERROR: Escaping the return of a proj to a mut is not allowed. Need to copy.
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = f(&p1);
+    // p1 is projected, so it can be used again (after p2 dies)
+}
+
+fn tmp2() {
+    let mut p2;
+    {
+        let mut p1 = Point { x: 1, y: 2 };
+        p2 = f(&p1);
+    }
+}
+
+// ==========
+// Mut-Proj-Proj as return and formal parameters from Proj
+// =========
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(proj p: Point, proj u: Point): Point {
+    // u is not used
+    let mut x = p.x; // proj -> mut: forces reinitialization
+    let mut y = p.y; // proj -> mut: forces reinitialization
+    *p.x = 10;
+    *p.y = 20;
+    Point { x, y }
+    // p // ERROR: Escaping the return of a proj to a mut is not allowed. Need to copy.
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, &p2);
+    // p1 is projected, so it can be used again
+    // p2 is projected, so it can be used again
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, &p2);
+    }
+}
+
+// ==========
+// Mut-Proj-Mut as return and formal parameters from Proj
+// =========
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(proj p: Point, mut u: Point): Point {
+    // u is not used
+    let mut x = p.x; // proj -> mut: forces reinitialization
+    let mut y = p.y; // proj -> mut: forces reinitialization
+    *p.x = 10;
+    *p.y = 20;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, p2);
+    // p1 is projected, so it can be used again
+    // p2 is moved, so it is not used anymore
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, p2);
+    }
+}
+
+// ==========
+// Mut-Proj-Imm as return and formal parameters from Proj
+// =========
+struct Point {
+    mut x: i32,
+    mut y: i32,
+}
+
+fn mut f(proj p: Point, imm u: Point): Point {
+    // u is not used
+    let mut x = p.x; // proj -> mut: forces reinitialization
+    let mut y = p.y; // proj -> mut: forces reinitialization
+    *p.x = 10;
+    *p.y = 20;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, p2);
+    // p1 is projected, so it can be used again
+    // p2 can be used again
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, p2);
+    }
+}
+
+// ========================================================================
+// ========================================================================
+// Store Imm in Struct from Proj
+// ========================================================================
+// ========================================================================
+
+// NOTE: proj binding + imm field -> imm access (imm is more restrictive than proj).
+// From a proj binding, imm fields remain immutable — the proj binding does not grant
+// mutable access to fields that are declared imm.
+
+// ==========
+// SINGLE CASE
+// ==========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(proj p: Point): Point {
+    let imm x = p.x; // imm field stays imm even under proj binding
+    let imm y = p.y;
+    // let mut x = p.x; // ERROR: imm fields cannot be accessed as mut. Need to copy.
+    // let proj x = &p.x; // ERROR: imm -> proj not allowed. Need to copy.
+    Point { x, y }
+    // p // ERROR: Escaping the return of a proj to a mut is not allowed. Need to copy.
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = f(&p1);
+    // p1 is projected, so it can be used again
+}
+
+fn tmp2() {
+    let mut p2;
+    {
+        let mut p1 = Point { x: 1, y: 2 };
+        p2 = f(&p1);
+    }
+}
+
+// ==========
+// Mut-Proj-Proj as return and formal parameters from Proj
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(proj p: Point, proj u: Point): Point {
+    // u is not used
+    let imm x = p.x; // imm field: always imm
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, &p2);
+    // p1 is projected, so it can be used again
+    // p2 is projected, so it can be used again
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, &p2);
+    }
+}
+
+// ==========
+// Mut-Proj-Mut as return and formal parameters from Proj
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(proj p: Point, mut u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let mut p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, p2);
+    // p1 is projected, so it can be used again
+    // p2 is moved, so it is not used anymore
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let mut p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, p2);
+    }
+}
+
+// ==========
+// Mut-Proj-Imm as return and formal parameters from Proj
+// =========
+struct Point {
+    imm x: i32,
+    imm y: i32,
+}
+
+fn mut f(proj p: Point, imm u: Point): Point {
+    // u is not used
+    let imm x = p.x;
+    let imm y = p.y;
+    Point { x, y }
+}
+
+fn tmp1() {
+    let mut p1 = Point { x: 1, y: 2 };
+    let imm p2 = Point { x: 3, y: 4 };
+    let mut p3 = f(&p1, p2);
+    // p1 is projected, so it can be used again
+    // p2 can be used again
+}
+
+fn tmp2() {
+    let mut p3;
+    let mut p1 = Point { x: 1, y: 2 };
+    {
+        let imm p2 = Point { x: 3, y: 4 };
+        p3 = f(&p1, p2);
+    }
+}
\ No newline at end of file
diff --git a/docsrc/examples/eter-semantics/illegal1.txt b/docsrc/examples/eter-semantics/illegal1.txt
new file mode 100644
index 0000000..e91e0c0
--- /dev/null
+++ b/docsrc/examples/eter-semantics/illegal1.txt
@@ -0,0 +1,9 @@
+fn tmp(proj x: i32, proj y: i32) {
+    x = &y;
+}
+fn main() {
+    let mut x: i32 = 1;
+    let mut y: i32 = 2;
+    tmp(&x, &y);
+    // UB: x and y are mutable aliases of the same memory location
+}
diff --git a/docsrc/examples/eter-semantics/not-compile-mut-iter.txt b/docsrc/examples/eter-semantics/not-compile-mut-iter.txt
new file mode 100644
index 0000000..9401ba4
--- /dev/null
+++ b/docsrc/examples/eter-semantics/not-compile-mut-iter.txt
@@ -0,0 +1,37 @@
+struct Iter {
+    mut data: [i32; 3],
+    mut cursor: usize,
+}
+fn mut iter(mut x: [i32; 3]): Iter<i32, 3> { Iter { data: x, cursor: 0 } }
+fn mut collect(mut it: Iter<i32, 3>): [i32; 3] { it.data }
+fn proj get(proj it: Iter<i32, 3>, fix i: i32): i32 { it.data[i] }
+fn next(proj it: Iter<i32, 3>): i32 {
+    let i = it.cursor;
+    if i >= 3 { abort(); }
+    *it.cursor = i + 1;
+    ret it.data[i];
+}
+
+fn main() {
+    let mut x: [i32; 3] = [1, 2, 3];
+    let mut it: Iter<i32, 3> = iter(x); // `x` is moved into the iterator
+    it.data[0] = 100;
+
+    let proj tmp = get(&it, 0);
+    let proj tmp2 = next(&it); // ERROR: it is already projected you cannot project it again
+    // UB: tmp and tmp2 would point to the same memory location
+
+
+
+    // -------------------------------------------------------------------------------
+    *tmp2 += 10;
+    // `el` dead (it's not used anymore), so you can use `it` again.
+
+    while proj el2 = next(it) {
+        // `it` is projected, you can't mutate `data` through it.
+        *el2 += 10;
+    }
+
+    // `it` returns alive, so you can continue using it.
+    x = collect(it);
+}
\ No newline at end of file