Question: `is_isomorphic_to` vs `==`

[lengyijun]

forall Term M N, if M is_isomorphic N => M == N

After some unittest, the proposition always stand.
Is there two terms M N where M is_isomorphic N but M != N

    let term1 = abs(Var(1)); // λ 1
    let term2 = abs(Var(2)); // λ 2
    let term3 = abs(Var(1)); // λ 1

    assert_eq!(term1.is_isomorphic_to(&term2), false);
    assert_eq!(term1.is_isomorphic_to(&term3), true);

    assert_eq!(term1 == term2, false);
    assert_eq!(term1 == term3, true);

    assert_eq!(&term1 == &term2, false);
    assert_eq!(&term1 == &term3, true);

    assert!(abs(Var(1)).is_isomorphic_to(&abs(Var(1))));
    assert!(!abs(Var(1)).is_isomorphic_to(&abs(Var(2))));
    assert!(!app(abs(Var(1)), Var(1)).is_isomorphic_to(&app(abs(Var(1)), Var(2))));
    assert!(app(abs(Var(1)), Var(1)).is_isomorphic_to(&app(abs(Var(1)), Var(1))));
    assert!(!app(abs(Var(1)), Var(1)).is_isomorphic_to(&app(Var(2), abs(Var(1)))));

    assert!(abs(Var(1)) == (abs(Var(1))));
    assert!(!(abs(Var(1)) == (abs(Var(2)))));
    assert!(!(app(abs(Var(1)), Var(1)) == (app(abs(Var(1)), Var(2)))));
    assert!(app(abs(Var(1)), Var(1)) == (app(abs(Var(1)), Var(1))));
    assert!(!(app(abs(Var(1)), Var(1)) == (app(Var(2), abs(Var(1))))));